Re: [isabelle] Proof by analogy and proof stability in Isabelle
"Transferring content" is exactly what an external representation of
proof objects would allow you to do. A format like Joe Hurd's
OpenTheory is designed primarily for transferring theorems between
completely different theorem provers, but the same idea could also be
useful for transferring theorems between different versions of the
*same* theorem prover.
And yes, this means
that at least a part of the versioning system becomes part of the
of the proof assistant.
The great thing about using proof objects is that you don't need to
trust any new code.
I think these issues should be transparent for the end user of the
proof assistant. It is maybe a good idea to use proof objects for
implementing the versioning system, but special cases like a change in
the proof object format (and there will be changes, trust me) and so
on must then be handled transparently by the system, otherwise it
becomes a pain for the user. Also proof objects are big and slow; most
users are willing to trade a vastly improved user experience for a
little bit of trust ...
My point is just that earlier snapshots of the theory development of
a theorem prover should be accessible from the current theory
development, no matter how that is implemented exactly. As an example,
take the theory of the real numbers.
A simple way of approaching this is to first introduce the natural
numbers, then rational numbers, then the real numbers. Later on we
introduce new natural numbers, new rational numbers and so on, so that
they are now subsets of each other. Actually, there is no need now any
more for the original natural numbers and so on. With a versioning
system we can throw them out of our newest version. In our newest
version, we can axiomatically introduce the real numbers (and
justifying this by pointing to the definition in an earlier version).
Also, there are several ways of introducing the real numbers. This is
no problem in our system, each way could belong to a different version.
So for the user, stuff that has been done 10 years ago, is still
there, unchanged, and it is accessible from the newest version of the
system. It is important that the versioning system is elegant and
easy to understand. It provides the high-level view of how the user
thinks about the system.
This archive was generated by a fusion of
Pipermail (Mailman edition) and