Email Gateway (Aug 17 2022 at 13:45): Email Gateway (Aug 17 2022 at 13:45):From: Sean McLaughlin <seanmcl@cmu.edu>
Hello,
I have a request to modify the proof terms from locales slightly.
Right now, theorems
which are proved in a locale setting, eg. Record.thy, only label the
Thm parts of the
proof tree with the short name of the theorem, eg. "induct", when
this is suppose
to signify "Record.product_type.induct".
See, eg. the proof of "Record.product_type.surjective_pairing"
It is rather difficult to figure out when I'm
dealing with a locale theorem, and then I can imagine when two
locales are open
at once and this will be doubly confusing. Even if only one locale
is open, it's an ugly
hack to figure out which "induct" you mean, as there are many.
Would marking the Thm nodes in this way be a problem? If so, please
suggest
a workaround.
Thanks,
Sean
Email Gateway (Aug 17 2022 at 13:45):From: Makarius <makarius@sketis.net>
Note that "Record.product_type.induct" is used for the exported version of
that fact.
Anyway, internal theorem names are little more than comments, providing
some hints about the context where the fact had been derived. All you can
do at the moment is to unfold the derivation to get the actual proof term.
At some point we might establish a clear one-to-one correspondence of
theorem identifiers and (closed) derivations, but this will probably be
something like "induct4711".
Makarius
Email Gateway (Aug 17 2022 at 13:45):From: Clemens Ballarin <ballarin@in.tum.de>
Sean McLaughlin wrote:
PThm(("Record.product_type.induct",_),...)
OK. But note that things are not a simple as that. In general,
theorems added to the context are instances of theorems stored in the
locale. Additionally, if the theorem was generated via interpretation
(commands interpretation and interpret) its hypotheses are replaced by
hypotheses of the context.
Clemens
Email Gateway (Aug 17 2022 at 13:45):From: Clemens Ballarin <ballarin@in.tum.de>
Hi Sean,
apparently, you are using Isabelle 2004, which is not going to be
modified any more.
Apart from that, I haven't understood whether you are talking about
accessing the exported version of a locale theorem, which is added to
the theorem database of the theory, or about the theorem that is added
to the proof context when entering a locale via "theorem (in L)", say.
Clemens
Email Gateway (Aug 17 2022 at 13:45):From: Sean McLaughlin <seanmcl@cmu.edu>
Hi Clemens,
I mean the latter. the proof tree is labeled, eg.
PThm(("induct",_),_,_..) instead of
PThm(("Record.product_type.induct",_),...)
If this is the same in 2005, my request is still open. I'll try to get
the new version working today.
Best,
Sean
Email Gateway (Aug 17 2022 at 13:45):From: Makarius <makarius@sketis.net>
It is more or less the same, ignoring the fact that Record.product_type no
longer exists -- it was used in the record package of Isabelle2004, but
this is done differently in Isabelle2005 (more efficiently).
As pointed out before, names of closed derivations do not have an
authentic formal status. This is a legacy problem in Isabelle, because
people are used to reuse theorem names at will -- even rebind theorems
after a theory has been ``finished''.
You should be able to ignore this problem. Just build your own table of
closed derivations indexed by the resulting proposition (using structure
Termtab). Then you can share proofs of theorems without relying on
particular naming schemes.
Makarius
Last updated: May 03 2024 at 08:18 UTC