Email Gateway (Aug 17 2022 at 13:45): Email Gateway (Aug 17 2022 at 13:45):From: Robin Green <greenrd@greenrd.org>
A question about transforming Isabelle proofs into really elementary,
long-winded form:
I have not used Isabelle yet, but I have read in three places that
Isabelle is designed to support many different logics and theories by
having a relatively simple core language upon which everything else is
implemented. It should, therefore, be possible to get Isabelle to output
a proof _entirely_ in this core language (i.e. so that it uses only the
very primitive notation from this core language, and only the most
elementary possible inferences are used, and no other files are referred
to), so that it can be independently verified by a very small,
easy-to-reason-about proof verifier. (Of course that still leaves the
question of whether the translation is correct, but let's ignore that
for now.)
When I talk about "the most elementary possible inferences", I am
thinking of something like Metamath[1], which is apparently based
entirely on simple substitution rules. In other words, emphatically not
(non-trivial) tactics.
In [2], I found a tantalising hint which suggests that this feature
became available in Isabelle 99:
"The Isabelle 98 version is used in this thesis, although a later
version (Isabelle99) has since been released. These recent versions
of Isabelle support the construction and export of proof derivations, a
feature that was not available in early versions of Isabelle."
However, I've been unable to ascertain, by browsing the documentation,
where this export feature that Watson refers to, is. Is it there but
undocumented, have I missed it, or have I misunderstood what it is? Or
is it simply not there?
Email Gateway (Aug 17 2022 at 13:45):From: Makarius <makarius@sketis.net>
On Thu, 12 Jan 2006, Robin Green wrote:
A question about transforming Isabelle proofs into really elementary,
long-winded form:
In [2], I found a tantalising hint which suggests that this feature
became available in Isabelle 99:
See Stefan Berghofer's thesis for a slightly more up-to-date report on
proof terms (based on lambda calculus) for Isabelle/Pure. The Introduction
and chapter 2 should give you some idea how this looks like.
Stefan Berghofer. Proofs, Programs and Executable Specifications in
Higher Order Logic. Ph.D. thesis, Institut für Informatik, Technische
Universität München, 2003.
http://www4.in.tum.de/~berghofe/papers/phd.pdf
When I talk about "the most elementary possible inferences", I am
thinking of something like Metamath[1], which is apparently based
entirely on simple substitution rules. In other words, emphatically not
(non-trivial) tactics.
I would consider the Metamath format slightly low-level, with adhoc
handling of bound variable scopes; lambda calculus provides a more
abstract and clean notion of variable binding and substitution.
Also note that the actual primary proof format for Isabelle is that of the
Isar proof language, which admits writing proofs in a human-readable
fashion. Needless to say, everything will end up as a primitive internal
proof object eventually, but normally these are getting too large to
inspect them directly. This is why humans would normally stay at the
level of Isabelle/Isar proof documents -- printed in LaTeX/PDF.
Makarius
Email Gateway (Aug 17 2022 at 13:45):From: Robin Green <greenrd@greenrd.org>
Replying to my own post -
My apologies. I read the paragraph I quoted too hastily and
misunderstood it! Dr. Watson has informed me that the export of proof
derivations _was_ supported in Isabelle 98 (not Isabelle 99 as I misread
it) - and is covered in his thesis, from which that quotation was taken.
(Any further information not covered in that thesis would of course be
appreciated.)
Last updated: May 03 2024 at 04:19 UTC