Re: [isabelle] "Clash of specification" error



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

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 at 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






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