[isabelle-dev] including raises Attempt to perform non-trivial merge of theories
kuncar at in.tum.de
Wed Aug 14 18:55:14 CEST 2013
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).
Now, I suppose that the theorem that is being registered by
[transfer_rule] always lives in the theory where the attribute is
applied and thus the other theorems used for preprocessing don't have to
be explicitly transferred to a higher theory. This is true, for example,
when declare foo[transfer_rule] is used.
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?
More information about the isabelle-dev