Re: [isabelle] "Clash of specification" error



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.