Email Gateway (Aug 19 2022 at 09:06): Email Gateway (Aug 19 2022 at 09:06):From: Lawrence Paulson <lp15@cam.ac.uk>
As I see it, there are advantages to both interfaces. And everything is accessible from ML simply because it is the implementation language, although of course this access may not be very convenient. I think it's generally accepted these days that the ML level really is more appropriate for development than for ordinary reasoning. It isn't realistic to support both Isar and the ML level as the day-to-day user interface; even with unlimited resources, such duplication wouldn't be very elegant.
Isabelle has undergone very rapid change over the years, and this has meant leaving a lot of old practices behind. I know that it has caused users difficulties in the past, and it's unfortunate, but maintaining upwards compatibility is also very difficult. As one of the earliest Isabelle users, you naturally feel this much more than others do.
Larry
Email Gateway (Aug 19 2022 at 09:07):From: Makarius <makarius@sketis.net>
Actually, the Prover IDE supports both Isabelle/Isar and Isabelle/ML
pretty well -- note that Isabelle/ML needs to be distinguished from the ML
bootstrapping environment to get the Isabelle/Pure/Isar implementation up
and running.
You can even imitate the proof style from the 1990-ies like this:
apply (tactic {* my_tac @{context} 7 *})
Its definitely not elegant, and there is little reason to use this form
today. It is better to use method_setup to define your own application
specific proof methods first, and then use them in the proofs.
Makarius
Email Gateway (Aug 19 2022 at 09:07):From: Jeremy Dawson <jeremy@rsise.anu.edu.au>
Larry,
I take your first point, that "everything is accessible from ML", but
in a practical sense, I would say it's not because the code is so
difficult to understand. (Much more difficult than either Isabelle as
it was in 1997, or HOL, to give examples within my experience.)
In a way, my first contribution to this thread was to make it clear that
both "development" and "ordinary reasoning" are intertwined - there was
quite a lot of "development" involved in getting the right combination
of compound tactics and proof steps to avoid a proof script which would
have been 10000 lines long.
The bigger issue is that pen and paper proofs I do and publish in a
journal will be available as long as people want to read them. The
Isabelle proofs I do are in Isabelle 2005, and include theory and ML
files from 1997, and so will in the future be inaccessible to anyone who
doesn't (or can't) install Isabelle 2005 (which only seems to work with
one particular version of PolyML). Given the philosophy of Isabelle
developers, prospective users need to be warned that if they want to
write proofs which will be accessible to future researchers, they need
to be done in print.
Finally, it's worth pointing out that no one in this thread has actually
come up with a suggestion about how to do the sort of proof which was
the subject of my original post other than using Standard ML (which, I
understand, was designed for exactly that purpose).
Jeremy
Lawrence Paulson wrote:
Email Gateway (Aug 19 2022 at 09:07):From: Makarius <makarius@sketis.net>
On Tue, 20 Nov 2012, Jeremy Dawson wrote:
In a way, my first contribution to this thread was to make it clear that
both "development" and "ordinary reasoning" are intertwined - there was
quite a lot of "development" involved in getting the right combination
of compound tactics and proof steps to avoid a proof script which would
have been 10000 lines long.
This is why I have never separated Isabelle/Isar and Isabelle/ML in that
sense, they are just two different languages of the Isabelle user-space.
My first command implemented on the Isar toplevel was 'ML'.
Isabelle/ML happens to be used much less in applications these days,
though, and this is no problem, merely an indication that the abstractions
of Isar do most of your work already without extra tinkering in ML.
Anyway, I've pointed to the Isar command 'method_setup' already. If you
look it up in the isar-ref or implementation manual, and then look at 5-10
examples in the library, you should rather quickly get an idea how to
define your own basic proof tools, like in the old ML-only times of
Isabelle in the 1990-ies.
The bigger issue is that pen and paper proofs I do and publish in a
journal will be available as long as people want to read them. The
Isabelle proofs I do are in Isabelle 2005, and include theory and ML
files from 1997, and so will in the future be inaccessible to anyone who
doesn't (or can't) install Isabelle 2005 (which only seems to work with
one particular version of PolyML). Given the philosophy of Isabelle
developers, prospective users need to be warned that if they want to
write proofs which will be accessible to future researchers, they need
to be done in print.
Users just need to be told about AFP, to preserve things in the longer
term. (AFP does not accept ancient 1900-style scripts.)
Finally, it's worth pointing out that no one in this thread has actually
come up with a suggestion about how to do the sort of proof which was
the subject of my original post other than using Standard ML (which, I
understand, was designed for exactly that purpose).
We will come back to this on-topic on the original thread. So far I've
skimmed a little over these theories by Christoph Lange, and it looks
mostly like a conventional "Isar deflation" job, not old-style ML
tinkering.
Makarius
Email Gateway (Aug 19 2022 at 09:07):From: Lawrence Paulson <lp15@cam.ac.uk>
I think it's a great pity that you are using such an elderly version of Isabelle.
If you have a lot of legacy code that simply can't be ported, or an application where it works really well, okay. But for general proofs, there is simply no comparison between the Isabelle of today and one that is seven years old. Sledgehammer, counterexample finding, a very powerful function definition package, lots and lots of AFP theories… You shouldn't forego all of those.
Larry
Email Gateway (Aug 19 2022 at 09:07):From: Jeremy Dawson <jeremy@rsise.anu.edu.au>
Larry,
I don't suppose the legacy code simply can't be ported, any more than it
can't be translated into HOL. But when I started to port it from
Isabelle2005 to Isabelle2007 (still using ML tactics) I quickly gave
up. I expect it would be much worse now.
And although it seems as though the documentation is more extensive now
than it was then, to learn Isar I would anticipate having some
questions. And the sort of answers I've had in the past to questions
("look at Makarius's thesis") aren't encouraging. The point is that to
contemplate converting everything to Isar I need to _know_ that help
will be available.
And anyway, what is the point of a system where you write tactics and
then wrap them up as required to give them the type required by
method_setup, rather than just write tactics? (This is of course a
question to which the answer might be apparent if there was a more
accessible description of the structure of an Isar proof than Makarius's
thesis). Or learning something as totally weird as the grammar of the
Isar language?
Cheers,
Jeremy
Lawrence Paulson wrote:
Email Gateway (Aug 19 2022 at 09:08):From: Lawrence Paulson <lp15@cam.ac.uk>
There is no doubt that the APIs have changed rapidly over the years, in large part to accommodate user requests (in particular, for all declarations to work within locales). It certainly does make life difficult for developers.
There is a significant philosophical difference between Isabelle and HOL. I had always intended (perhaps even in 1986) that users should not have to write code in order to prove theorems. So I had no difficulty with a non-programmable notation for proofs, especially structured proofs, which (once you get the hang of them) make complicated proofs easier to write, understand and modify.
Mike Gordon expressed the difference between HOL and Isabelle succinctly: HOL can be seen as an API for coding proof procedures, while Isabelle is an interactive theorem prover that you use right out of the box. I know that this doesn't help at all with your situation.
Larry
Email Gateway (Aug 19 2022 at 09:08):From: Jeremy Dawson <jeremy@rsise.anu.edu.au>
Lawrence Paulson wrote:
There is no doubt that the APIs have changed rapidly over the years, in large part to accommodate user requests (in particular, for all declarations to work within locales). It certainly does make life difficult for developers.
There is a significant philosophical difference between Isabelle and HOL. I had always intended (perhaps even in 1986) that users should not have to write code in order to prove theorems. So I had no difficulty with a non-programmable notation for proofs, especially structured proofs, which (once you get the hang of them) make complicated proofs easier to write, understand and modify.
Larry,
This being so, it's very fortunate that you did such a good job of
producing a programmable notation for proofs, in which one can write
code in order to prove theorems, when necessary (granted that it's
mostly not necessary).
Mike Gordon expressed the difference between HOL and Isabelle succinctly: HOL can be seen as an API for coding proof procedures, while Isabelle is an interactive theorem prover that you use right out of the box. I know that this doesn't help at all with your situation.
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 ??
Jeremy
Larry
On 21 Nov 2012, at 02:50, Jeremy Dawson <jeremy@rsise.anu.edu.au> wrote:
Larry,
I don't suppose the legacy code simply can't be ported, any more than it can't be translated into HOL. But when I started to port it from Isabelle2005 to Isabelle2007 (still using ML tactics) I quickly gave up. I expect it would be much worse now.
And although it seems as though the documentation is more extensive now than it was then, to learn Isar I would anticipate having some questions. And the sort of answers I've had in the past to questions ("look at Makarius's thesis") aren't encouraging. The point is that to contemplate converting everything to Isar I need to _know_ that help will be available.
And anyway, what is the point of a system where you write tactics and then wrap them up as required to give them the type required by method_setup, rather than just write tactics? (This is of course a question to which the answer might be apparent if there was a more accessible description of the structure of an Isar proof than Makarius's thesis). Or learning something as totally weird as the grammar of the Isar language?
Cheers,
Jeremy
Lawrence Paulson wrote:
I think it's a great pity that you are using such an elderly version of Isabelle.
If you have a lot of legacy code that simply can't be ported, or an application where it works really well, okay. But for general proofs, there is simply no comparison between the Isabelle of today and one that is seven years old. Sledgehammer, counterexample finding, a very powerful function definition package, lots and lots of AFP theories… You shouldn't forego all of those.
Larry
Email Gateway (Aug 19 2022 at 09:08):From: Lawrence Paulson <lp15@cam.ac.uk>
You still have the capacity to code your own proof procedures; ML is just one level down. And you get a much more readable proof language.
Some years ago, I translated a lot of proofs from HOL to Isabelle. The HOL proofs were opaque blocks of tactics, while in the corresponding structure proof you could see (even if you knew little of the Isar language) which local facts were available for use and what had to be proved. And almost certainly, creating those opaque blocks of tactics required much more effort, because the old ML style (whether in HOL or Isabelle) isn't very good at forward reasoning.
Larry
Email Gateway (Aug 19 2022 at 09:08):From: Makarius <makarius@sketis.net>
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).
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).
Makarius
Email Gateway (Aug 19 2022 at 09:09):From: Makarius <makarius@sketis.net>
The situation is a bit more general than this, and it is hard to arrange
Isar vs. ML in "levels" in particular. Both are intertwined, cf. my
explanation of Isabelle/Isar and Isabelle/ML as as the Yin and Yang of
Isabelle
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2012-April/msg00066.html
In general Isar vs. its embedded languages works like this:
* Isar is the main framework of Isabelle to integrate many
other languages.
* The Isar languages for specifications (e.g. 'theorem', 'definition',
'function') and proofs (e.g. 'fix', 'assume', 'show' ...) are the
primary applications of the Isar framework.
* The logical language (Pure types/terms/propositions with specific HOL
notation) is another important embedded language, cf. the quotes that
have been around this language even in the ancient ML-only times of
Isabelle in the 1990-ies.
* ML is embedded into Isar in a similar manner, but at the same
time it is the implementation language of Isar. Moreover, ML quoted
inside Isar can antiquote logic/Isar expressions. So the image for
that is http://en.wikipedia.org/wiki/File:Yin_and_Yang.svg
In everyday life you don't use the ML inside Isar a lot, but you can
whenever you need to. It is more convenient than the ancient ML toplevel
ever was. In Isabelle/jEdit you also have substantial IDE integration for
this ML inside Isar.
Makarius
Email Gateway (Aug 19 2022 at 09:10):From: Jeremy Dawson <jeremy@rsise.anu.edu.au>
On 11/22/2012 10:32 PM, Lawrence Paulson wrote:
You still have the capacity to code your own proof procedures; ML is just one level down. And you get a much more readable proof language.
Larry,
While this is true, I did a lot of it a few years ago, and kept finding
things not working. Mostly to do with theories - in one way or another.
Impossible (for me or, in one case, for the developer I spoke to) to
work out exactly what was going on.
Some years ago, I translated a lot of proofs from HOL to Isabelle. The HOL proofs were opaque blocks of tactics, while in the corresponding structure proof you could see (even if you knew little of the Isar language) which local facts were available for use and what had to be proved. And almost certainly, creating those opaque blocks of tactics required much more effort, because the old ML style (whether in HOL or Isabelle) isn't very good at forward reasoning.
You're certainly right about opaque blocks of tactics - but having to
execute a proof to see the intermediate steps has got to be the price
you pay for not having to write down all those intermediate steps. This
whole thread started with the topic of an (I assume) Isar proof which
was too long to be readable.
I don't know what local facts (or indeed facts generally) are. I
suspect it's part of the larger question of what the state of a part
completed Isar proof consists of, and how it related to what you see on
the screen. I understood (a year or two ago) that this was not documented.
Jeremy
Larry
On 21 Nov 2012, at 22:31, Jeremy Dawson<jeremy@rsise.anu.edu.au> 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 ??
Email Gateway (Aug 19 2022 at 09:10):From: Jeremy Dawson <jeremy@rsise.anu.edu.au>
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
Email Gateway (Aug 19 2022 at 09:12):From: Makarius <makarius@sketis.net>
On Fri, 23 Nov 2012, Jeremy Dawson wrote:
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).
There is indeed an ambiguity: "Isar" can mean several things at several
scales looking at it. And the "Isar framework" is still more vast and
spacious than the things mentioned in the paragraph above.
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
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.
Makarius
Email Gateway (Aug 19 2022 at 09:13):From: Jeremy Dawson <jeremy@rsise.anu.edu.au>
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")
doneAnother 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
Email Gateway (Aug 19 2022 at 09:13):From: Makarius <makarius@sketis.net>
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
Email Gateway (Aug 19 2022 at 09:14):From: Jeremy Dawson <jeremy@rsise.anu.edu.au>
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
Email Gateway (Aug 19 2022 at 09:21):From: Jens Doll <jd@cococo.de>
Hello all,
when viewing the file Vickrey.thy from Tim I almost fell from my chair.
It has 22 pages of code and that seems to be a normal length for Isabelle.
Does anyone know how to shorten these artefacts or could someone explain
to me why proofs have to be that long?
Jens
Email Gateway (Aug 19 2022 at 09:22):From: Jeremy Dawson <jeremy@rsise.anu.edu.au>
Jens,
I don't know if this is a factor in this particular set of proofs, but
often a particular sequence of proof steps is reused repeatedly.
In such a case it is advantageous not to have to write them all down
repeatedly, but to reuse them.
The Standard ML interface to Isabelle is ideally suited to this
purpose. Unfortunately its use has become actively discouraged in
recent years.
To illustrate, here are some bits of a proof script of mine which makes
good use of the Standard ML interface.
fun mctrtac sg st = FIRST [ atac sg, (match_tac [mstrctr.ctr] sg),
((resolve_tac [mstrctr.Comma, mstrctr.Star] THEN_ALL_NEW mctrtac) sg),
(rtac mstrctr.same sg) ] st ;
fun dvi_ctr_tacs dths = [
(rtac ex_conjI), (rtac mseqctr.I), mctrtac, mctrtac,
(eresolve_tac [der_asm, dd1th] THEN_ALL_NEW
resolve_tac dths THEN_ALL_NEW ssai_tac) ] ;
fun init_dvi_ctr_tacs dths = [
(* ensure only desired occurrence of rule is expanded *)
Clarsimp_tac, dtac trans, (clarsimp_tac (cesimps rule_defs)),
rtac refl, Clarsimp_tac,
(SELECT_GOAL (EVERY [
(* split up say F delible from (X,Y),Z |- W into cases:
F (with stars) is X,Y or Z, or F is delible from X,Y,Z or W *)
(REPEAT_SOME (eresolve_tac [mseqctr.elim,
mstrctr_CommaR, mstrctr_StarR, mstrctr_IR]
THEN_ALL_NEW Clarsimp_tac)),
(* when deletion to substituted variable in rule *)
TRYALL (EVERY' (dvi_ctr_tacs dths)) ])) ] ;
fun xstacs th = [
(rtac ex_conjI 1), (etac dd1th 2),
((rtac th THEN_ALL_NEW ssai_tac) 2),
(rtac mseqctr.I 1), mctrtac 1, mctrtac 1 ] ;
val th = rdp (tn [dca1, dppsA, dica1, dassoc]) ;
in the above, each additional theorem in the list of arguments to tn
involves several proof steps
val ctr_assoc_tacs = [
(EVERY' (init_dvi_ctr_tacs [dassoc]) 1),
(EVERY (xstacs ([dassoc, dassoc] MRS duA2))),
(EVERY (xstacs th)) ] ;
(and twelve more rather like ctr_assoc_tacs, just a bit different)
val ctr_tacs = [ EVERY init_ctr_tacs,
EVERY ctr_assoc_tacs,
EVERY ctr_ica1_tacs, EVERY ctr_ica2_tacs,
EVERY ctr_ics1_tacs, EVERY ctr_ics2_tacs,
(EVERY' (init_dvi_ctr_tacs [dastars]) 1),
(EVERY' (init_dvi_ctr_tacs [dassA]) 1),
EVERY ctr_ca1_tacs, EVERY ctr_ca2_tacs,
EVERY ctr_cs1_tacs, EVERY ctr_cs2_tacs,
EVERY ctr_rstars_tacs, EVERY ctr_rssA_tacs ] ;
If I had written this out in the modern style (using Isar) the above
would expand to thousands, probably tens of thousands, of lines of code.
Cheers,
Jeremy Dawson
Jens Doll wrote:
Email Gateway (Aug 19 2022 at 09:23):From: Christian Sternagel <c-sterna@jaist.ac.jp>
Almost always, it is possible to considerably shorten proofs by use (and
proper setup) of automated techniques (maybe even more so when using
Isabelle/ML). The other extreme is to explicitly write every single step
in Isar (as I know from myself and many students I taught, mostly
beginners use this kind of proofs... of course it also depends on your
intended audience).
In my opinion both extremes are bad. It is an art (as is often pointed
out in Isar related manuals) to write Isar proofs that are readable yet
not too verbose. But if you master this art, the gain is that others can
actually read your proofs and follow the steps without even starting
Isabelle (which is definitely not the case with the technique shown by
Jeremy; so I would rather use that technique that are considered
"trivial" by humans... but then again humans are often wrong in their
initial judgment of what is trivial ;)).
I guess what I want to say is that no, proofs do not have to be
exceedingly long in many cases, but sometimes long versions (or rather
versions of appropriate length) are much better to read and maintain.
cheers
chris
Email Gateway (Aug 19 2022 at 09:24):From: Makarius <makarius@sketis.net>
As far as I am concerned, I never discouraged the use of Isabelle/ML, it
merely came out of use as proof scripting languages, because there are
better ways these days. Christian Sternagel has already hinted at the
fine art to combine structured Isar proof elements, and an assorted
collection with proof tools.
If you still want to have hard-core quick script hacking, the community
for that is centered around SSReflect, which is continuing traditions of
APL for proof recording. The scripts then come out very tight and terse,
by experts for experts.
I am still keen to seen such a quick-hacking approach turned into proper
use for an advanced Prover IDE: instead of recording the gesticulation of
the author in the script, it would produce a nice structured, readable,
maintainable proof document.
Makarius
Email Gateway (Aug 19 2022 at 09:25):From: Jeremy Dawson <jeremy@rsise.anu.edu.au>
Makarius,
My understanding has been that you - or someone - introduced new
features in Isabelle which were accessible only from Isar, not from the
Standard ML interface.
In my book this discourages the use of Standard ML, and also provides an
explanation for it having "come out of use", regardless of its relative
merits as a user interface language.
I don't understand your reference to SSReflect. How would that help me
do Isabelle proofs?
Jeremy
Last updated: Apr 20 2024 at 08:16 UTC
