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# 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);
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
