Re: [isabelle] theory_of_thm @{thm xxx}



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.

On 22/08/12 02:47, Peter Lammich wrote:
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









This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.