Re: [isabelle] "Clash of specification" error



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

-- 

PGP available:
http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

Attachment: signature.asc
Description: OpenPGP digital signature



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