Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] "Clash of specification" error

view this post on Zulip Email Gateway (Aug 22 2022 at 14:39):

From: Dominic Mulligan via Cl-isabelle-users <cl-isabelle-users@lists.cam.ac.uk>
Hi,

It seems I'm unable to use the Word_Enum theory from the AFP Word
library and List_lexord theory from the HOL Library concurrently as
Isabelle-2016 raises the following exception when processing
dependencies:

Clash of specifications for less:
"List_lexord.ord_list_inst.less_list_def"⌂
"Prefix_Order.ord_list_inst.less_list_def"⌂

Minimum example:

theory
Error_Monad
imports
Main
"$AFP/Word_Lib/Word_Enum"
"~~/src/HOL/Library/List_lexord"
begin

(* XXX *)

end

(In my development, I'm importing List_lexord in X.thy and Word_Enum
in Y.thy with a dependency between the two.)

Is there a way around this?

Thanks,
Dominic

view this post on Zulip Email Gateway (Aug 22 2022 at 14:39):

From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi Dominic,

Every type class can be instantiated only once for each type. For lists, there are two
different instantiations in different theories in HOL/Library: List_lexord defines the
order on lists to be lexicographic and Prefix_Order defines the order to be by prefix.
Therefore, you cannot import both into one theory, but this happens in your example,
because Word_Lib transitively imports the theory Prefix_Order. There's no way around this.

Best,
Andreas

view this post on Zulip Email Gateway (Aug 22 2022 at 14:39):

From: Dominic Mulligan via Cl-isabelle-users <cl-isabelle-users@lists.cam.ac.uk>
Hi Andreas,

Thanks for the reply.

After a bit of digging through the Word_Lib code it seems that
Prefix_Order is being imported in WordBitwise_Signed, which itself
does not use any of the functionality provided by Prefix_Order itself,
but as it is quite a basic theory in Word_Lib, the library becomes
"infected" with this type class instantiation along with any other
code that imports any Word_Lib theory. Rather, the only theories that
seems to rely on Prefix_Order at all is WordLemmas and theories that
depend on it.

Therefore, unless I'm missing something important, the import of
Prefix_Order in WordBitwise_Signed can be removed and be placed in
WordLemmas with no effect on the functionality of the library,
reducing the amount of "infected" code and allowing users to split out
e.g. Word_Enum in contexts where List_lexord is also imported.

Thanks,
Dominic

view this post on Zulip Email Gateway (Aug 22 2022 at 14:39):

From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi Dominic,

Indeed, you are right. If you are only interested in Word_Enum, then Prefix_Order does not
seem to be necessary. I've committed the appropriate change to the AFP testboard

https://bitbucket.org/isa-afp/afp-testboard/commits/e0f29efc9e56a2c94424263832ab7f833e63ffba

If this does not cause any problems, I'll push it to AFP-devel such that in the next AFP
release (for Isabelle2016-1) you can use Word_Enum in combination with List_lexord.

Best,
Andreas

view this post on Zulip Email Gateway (Aug 22 2022 at 14:40):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Andreas,

Indeed, you are right. If you are only interested in Word_Enum, then
Prefix_Order does not seem to be necessary. I've committed the
appropriate change to the AFP testboard

https://bitbucket.org/isa-afp/afp-testboard/commits/e0f29efc9e56a2c94424263832ab7f833e63ffba

If this does not cause any problems, I'll push it to AFP-devel such that
in the next AFP release (for Isabelle2016-1) you can use Word_Enum in
combination with List_lexord.

that is surely a step in the right direction.

But also note that only a dozen of lemmas on WordLemmas requires
Prefix_Order, and these seem to be not related to words or bits at all, e.g.

lemma sublist_equal_part:
"xs ≤ ys ⟹ take (length xs) ys = xs"
by (clarsimp simp: prefix_def less_eq_list_def)

It would be much better to move these to Prefix_Order and relieve
Word_Lib of that dependency altogether.

Cheers,
Florian

Best,
Andreas

On 17/11/16 16:57, Dominic Mulligan wrote:

Hi Andreas,

Thanks for the reply.

After a bit of digging through the Word_Lib code it seems that
Prefix_Order is being imported in WordBitwise_Signed, which itself
does not use any of the functionality provided by Prefix_Order itself,
but as it is quite a basic theory in Word_Lib, the library becomes
"infected" with this type class instantiation along with any other
code that imports any Word_Lib theory. Rather, the only theories that
seems to rely on Prefix_Order at all is WordLemmas and theories that
depend on it.

Therefore, unless I'm missing something important, the import of
Prefix_Order in WordBitwise_Signed can be removed and be placed in
WordLemmas with no effect on the functionality of the library,
reducing the amount of "infected" code and allowing users to split out
e.g. Word_Enum in contexts where List_lexord is also imported.

Thanks,
Dominic

On 17 November 2016 at 15:37, Andreas Lochbihler

<andreas.lochbihler@inf.ethz.ch> wrote:

Hi Dominic,

Every type class can be instantiated only once for each type. For lists,
there are two different instantiations in different theories in
HOL/Library:
List_lexord defines the order on lists to be lexicographic and
Prefix_Order
defines the order to be by prefix. Therefore, you cannot import both
into
one theory, but this happens in your example, because Word_Lib
transitively
imports the theory Prefix_Order. There's no way around this.

Best,
Andreas

On 17/11/16 16:22, Dominic Mulligan via Cl-isabelle-users wrote:

Hi,

It seems I'm unable to use the Word_Enum theory from the AFP Word
library and List_lexord theory from the HOL Library concurrently as
Isabelle-2016 raises the following exception when processing
dependencies:

Clash of specifications for less:
"List_lexord.ord_list_inst.less_list_def"⌂
"Prefix_Order.ord_list_inst.less_list_def"⌂

Minimum example:

theory
Error_Monad
imports
Main
"$AFP/Word_Lib/Word_Enum"
"~~/src/HOL/Library/List_lexord"
begin

(* XXX *)

end

(In my development, I'm importing List_lexord in X.thy and Word_Enum
in Y.thy with a dependency between the two.)

Is there a way around this?

Thanks,
Dominic

signature.asc

Last updated: Apr 26 2024 at 04:17 UTC