Email Gateway (Aug 22 2022 at 18:00): Email Gateway (Aug 22 2022 at 18:00):From: Ken Kubota <mail@kenkubota.de>
Am 15.08.2018 um 07:46 schrieb Michal Wallace <michal.wallace@gmail.com>:
for your 60000 elementary steps....
Some people actually do want that. One thing that draws people to
metamath.org,
for example, is that every single step is shown... The only rules are
syntax definition and substitution, and the people that
like metamath consider that an extremely important feature. On the other
hand, they have the good taste to break each
proof down into small chunks, so you rarely (?) see a proof that's more
than a screenful of text.
It would be desirable to have a mode in Isabelle in which for an automated proof
each single step is made explicit and displayed afterwards (or saved to disk in a file)
with full type information.
It shouldn't be too difficult to implement both modes, one without tracking
(for performance), and one with tracking (allowing one to follow each single
step).
You seem to be feeling a lot of frustration with Isabelle. I can't say I'm
not feeling similar frustrations, but
in my experience, that frustration is just a thing that happens when you
try to really understand any
big complicated system. The way through it is to be patient, ask questions,
experiment, study what
other people have done (or what other people have asked, either here or
on stack overflow), and
just trust that eventually things that were confusing at first will
eventually start to make sense.
This isn't the case for HOL (HOL4). With the HOL handbook [Gordon and Melham, 1993]
(and an online tutorial) I was able to fully understand and work with the system
within 24 hours.
Generally speaking, with a clear and concise presentation of the concepts and the logic(s)
within a good documentation (and not many scattered papers) the principles of any large
system can be explained properly.
Maybe the Isabelle team should consider asking Andy Pitts to write a logic part
for Isabelle and Isabelle/HOL (as soon as no major changes are expected anymore)
with the same brilliance like that of the logic part of the HOL handbook.
Also... My impression (and I could be wrong about this) is that most of the
users of Isabelle are not just
going it alone, but are academics working closely with and being taught by
other people who are
intimately familiar with the system already. Nobody's written a "Learn You
an Isar for Great Good" and
there's not (yet) been a huge influx of curious outsiders blazing trails
for everyone else. So that
means people like you and me (who seem to be sometimes frustrated
outsiders) have on opportunity
to be the trailblazers -- the ones who subject ourselves to getting lost
for a while, knowing
that when we eventually do find our way, we can make it easier for the next
person.
This is exactly what I wrote some time ago on this list (concerning Isabelle,
not just Isar).
The theoretical foundation ([Paulson, 1988]) is excellent, and Isabelle is an
impressive software, but the documentation is a nightmare. In it, logical
foundations are mixed up with technical details. It has many references
to articles outside of the documentation (at least in earlier versions), forcing
one to struggle one's way through a jungle of numerous articles. I believe
it took me years just to find out that [Paulson, 1988] is the theoretical foundation.
The documentation should enable one to work with the software independently,
but in fact it is a supplementary reference for "academics working closely with
and being taught by other people who are intimately familiar with the system
already".
For references, please see: http://doi.org/10.4444/100.111
Ken Kubota
http://doi.org/10.4444/100
Email Gateway (Aug 22 2022 at 18:01):From: Ken Kubota <mail@kenkubota.de>
Carrying out proofs in Isabelle can be quite easy, but this is not the point.
A logician wants to know what actually happens below the surface,
i.e., what the logical concepts (foundations) are, and how the formulae
are represented internally (with full details such as type information).
For example, in order to avoid the inconsistency as presented on p. 2 of
http://andreipopescu.uk/pdf/compr_IsabelleHOL_cons.pdf
and quoted at
http://owlofminerva.net/kubota/r0-faq/
an additional check is made at run-time.
If I'm not mistaken, the current Isabelle version implements a run-time check on
whether a theory is well-formed based on the dependency relation
as defined on p. 8 in the paper linked above. (In other words, it is verified
that there are no circular definitions.)
Such an intricate logical concept - which differs from other existing systems -
should be mentioned in the manual, and preferably in a separate part on the logic
(in this case Isabelle/HOL).
Usually, avoiding inconsistencies is the task of the type system.
Additionally, in HOL, some extensions have restrictions on definitions
(see, e.g., [Gordon and Melham, 1993, p. 220, condition (iii)], or p. 33 of the online version
at http://freefr.dl.sourceforge.net/project/hol/hol/kananaskis-11/kananaskis-11-logic.pdf ),
which are verified prior to accepting the definition and concern only the definition itself,
not the whole theory.
Performing run-time checks (after the definitions were accepted) on the whole theory
is something completely different and should be announced prominently.
But this isn't the case, as far as I can see.
For references, please see: http://doi.org/10.4444/100.111
Ken Kubota
http://doi.org/10.4444/100
Email Gateway (Aug 22 2022 at 18:04):From: Tobias Nipkow <nipkow@in.tum.de>
Let me just add that one can also contribute to this envisaged AFP entry "Number
Theory Miscellany" once it is in place, not just now. The same is in principle
true for any AFP entry, although most of them don't have this library character,
and of course you have to liaise with their authors first.
Tobias
smime.p7s
Last updated: Apr 26 2024 at 01:06 UTC