Email Gateway (Aug 19 2022 at 08:20): Email Gateway (Aug 19 2022 at 08:20):From: Peter Lammich <lammich@in.tum.de>
Hi all,
consider the following toy example:
theory Scratch
imports Pure
begin
ML_val {*
theory_of_thm @{thm meta_mp}
*}
Output: val it = {Pure, Scratch:1}: theory
Why is Scratch contained in here? The theorem is defined in Pure, not in
Scratch.
Is there a way to reference to the theorem by name such that its theory
is the one it was defined in, and not the one the antiquotation occurs
in?
In my real application (using HOL instead of Pure), I get odd
"non-trivial theory-merge" exceptions, because "theory_of_thm @{thm
xxx}" contains too much.
Regards and thanks in advance for any help,
Peter
Email Gateway (Aug 19 2022 at 08:21):From: Thomas Sewell <Thomas.Sewell@nicta.com.au>
In principle, having @{thm meta_mp} live only in @{theory Pure} would
make perfect sense.
In practice, this would create a problem if you tried, say:
theory Scratch
imports A B
begin
ML_val {*
Thm.transitive @{thm A.eq1} @{thm B.eq2}
*}
How does Thm.transitive figure out an appropriate context for a rule
derived from A.eq1 and B.eq2?
To avoid this problem, A.eq1 and B.eq2 are "pulled" up into theory
Scratch when they are fetched, thus allowing derivation operations to
proceed without doing any interesting work.
There are other ways in ML to fetch these theorems in their original
context, at which point if you attempt resolution or similar you will
see the error "Attempt to perform non-trivial merge of theories" from
Pure/context.ML.
Yours,
Thomas.
Email Gateway (Aug 19 2022 at 08:21):From: Peter Lammich <lammich@in.tum.de>
Thanks Thomas.
In my particular case, I have implemented an attribute that also uses
theorems fetched from record types. The problem is, that the theory that
declares the record type does not import the theory that declares the
attribute.
For now, I solved the problem by fetching the theorems in their original
context, and then transferring them to HOL/Main, assuming that all
theorems that my attribute sees depend on a super-theory of Main, which
is realistic in my case.
Peter
Email Gateway (Aug 19 2022 at 08:21):From: Makarius <makarius@sketis.net>
The proper technical term for "pulled" is "transfer" in Isabelle
terminology. What you mention in a certain context needs to be understood
in the sense of that context. Formal entities with a back-reference to a
context certificate (theory stamp) need to be transferred explicitly,
unlike terms who might get re-checked implicitly. (Such system operations
are carefully implemented to be monotonic wrt. the theory context.)
The Isar source language alreadys transfers formal entities mentioned in
the text: notably 'thm' and @{thm} etc. so one never has to worry about
it.
In really ancient times we did not understand this important principle
yet, and there were many oddities coming from theorems with incomparable
theory stamps, or comparable theory stamps that were just too little for
the current context, say to perform an instantiation.
These problems are long forgotten, because the transfer principle is the
established way for such a long time already. (This is in disagreement
with the very first sentence above.)
Makarius
Email Gateway (Aug 19 2022 at 08:21):From: Makarius <makarius@sketis.net>
So why not make the imports right, according to what you do formally?
Makarius
Email Gateway (Aug 19 2022 at 08:21):From: Peter Lammich <lammich@in.tum.de>
Because this is not the "right" way from a modularization standpoint.
The theory that declares the record type and the theory that declares
the attribute are independent, so I see no need to import the one from
the other. The dependence is established by a third theory, importing
both, and using the attribute declared in the latter with a theorem
containing the record type declared in the former.
However, just introducing this (artificial, and on first glance
unnecessary) dependence might be the quickest way to solve the problem.
The cleanest (?) might be to manually transfer the theorems extracted
from the record type to the theory of the theorem that is passed to the
attribute (This theory should always include both, the theory of the
record type and the one declaring the attribute)
Email Gateway (Aug 19 2022 at 08:21):From: Makarius <makarius@sketis.net>
I can only guess what your overall structure is, but the latter also
sounds right to me. The function for that is Thm.transfer.
Makarius
Email Gateway (Aug 19 2022 at 08:21):From: Thomas Sewell <Thomas.Sewell@nicta.com.au>
Apologies for nitpicking, but there is room for us both to be right.
This might be a principled approach, and it has pragmatic merit and the
weight of tradition, but, in principle, there might be other valid
approaches.
For instance, a system like Isabelle could have theorems depend on lists
of theories, or equivalently construct meet/join objects in the theory
lattice. It would probably be inefficient and sometimes surprising, but
it could be done. I'm not saying that this is a good approach, I'm
saying that the vagueness of principle encompasses it.
Yours,
Thomas.
Email Gateway (Aug 19 2022 at 08:22):From: Makarius <makarius@sketis.net>
Until 1997 there was indeed an explicit join (merge) constructed for
incomparable theory stamps. This was a bit inefficient, and sometimes
occurred in surprising situations, so we discontinued it.
Nonetheless, the join (least upper bound of given theory stamps) is
sometimes not sufficient to do the job, it might be still too small for
the current context where you are working. Say you want to instantiate a
theorem with variables that have type class constraints, but the merge of
theories does not give you the required instance yet. (Such incidents did
happen in practical situations in the past and motivated the rethinking of
the concepts.)
The claim of the current Isabelle scheme of trivial merges of already
related theories + transfer to the context where you are working is that
it addresses all practical situations. I am ready to see counter examples
for that claim, if they exist.
Makarius
Last updated: Apr 19 2024 at 04:17 UTC