[isabelle-dev] including raises Attempt to perform non-trivial merge of theories

[Makarius]

On Wed, 14 Aug 2013, Ondřej Kunčar wrote:

> On 08/13/2013 04:19 PM, Andreas Lochbihler wrote:
>> Dear all,
>> 
>> in Isabelle abd760a19e22, I get the error "Attempt to perform
>> non-trivial merge of theories" when I include a bundle from another
>> theory and there are at least two imports.
>> In the attachment, there's an example.
>
> The problem happens in the function Transfer.abstract_equalities_transfer 
> where the theorem that is supposed to be registered by the attribute 
> [transfer_rule] is combined with other theorems (used for preprocessing) that 
> are stored in the theory data of the Transfer package (they are retrieved 
> through Transfer.get_relator_eq).

> But apparently it is not true for bundles. It seems that theorems that 
> are stored in a bundle still live in a theory where the bundle was 
> defined, and not in the theory where the attributes are applied (i.e., 
> where including is invoked). Shouldn't be the theorems that are stored 
> in a bundle transferred to a theory where including is invoked before 
> the attributes are applied to them?

The transfer business should indeed be done more deeply on the system side 
-- even bundles are just a client there.  Now that the "staleness" problem 
has disappeared from all our worries, the same should hold for transfer.

After two rounds of looking through it, I've devised the included change. 
It seems to address the situation exposed by Andreas, but breaks 
HOL/Quotient_Examples.thy here:

lift_definition fmember :: "'a ⇒ 'a fset ⇒ bool" (infix "|∈|" 50) is 
"λx xs. x ∈ set xs"
    parametric member_transfer by simp

exception THM 0 raised (line 404 of "thm.ML"):
   transfer: not a super theory
   bi_unique A  [bi_unique A]


This might be either a problem with "the context" on your side, or 
something else wrong in the system infrastructure.

I will look again soon, but am presently busy elsewhere.


 	Makarius
-------------- next part --------------
# HG changeset patch
# User wenzelm
# Date 1376944425 -7200
# Node ID d25b70614fe66f015dc0bede016d352484724a8f
# Parent  6cd0feb85e35d0133b7392969ba3851c7fe13682
always transfer thm where attributes are applied -- relevant for internal 'notes' (e.g. via bundle 'includes') in contrast to external 'notes' (cf. Proof_Context.retrieve_thms);

diff -r 6cd0feb85e35 -r d25b70614fe6 src/Pure/more_thm.ML
--- a/src/Pure/more_thm.ML	Mon Aug 19 20:47:09 2013 +0200
+++ b/src/Pure/more_thm.ML	Mon Aug 19 22:33:45 2013 +0200
@@ -407,7 +407,7 @@
 fun mixed_attribute f (x, th) = let val (x', th') = f (x, th) in (SOME x', SOME th') end;
 
 fun apply_attribute (att: attribute) th x =
-  let val (x', th') = att (x, th)
+  let val (x', th') = att (x, Thm.transfer (Context.theory_of x) th)
   in (the_default th th', the_default x x') end;
 
 fun attribute_declaration att th x = #2 (apply_attribute att th x);