Re: [isabelle] Theory name conflict



I've been too long to answer but it could anyway explain a little more the 
problem.

> Let us again revisit the actual situation:
> 
>   "~~/src/HOL/Imperative_HOL/Array"
>   "afp/thys/Collections/common/Array"
> 
> If I understand correctly, the problem is that fact names (also constant
> names?) in Collections shadow some in Imperative_HOL.  My intention is
> to refrain from any modification of the existing theories if there is
> »natural« way to do so.

In fact, all objects defined or imported by the last in the import list (the 
last read theory ?) are hidden.

For example, in the reverse situation:

    "afp/thys/Collections/common/Array"
    "~~/src/HOL/Imperative_HOL/Array"

where "Imperative_HOL/Array" imports "Heap_Monad" which imports "Heap",

    term Array.get
    thm Array.noteq_sym

    term Heap_Monad.Heap
    typ "'a Heap_Monad.Heap"

    thm Heap.addr_of_array_inj
    typ Heap.heap
    term Heap.empty

are all hidden, and so trying to import this:

    "afp/thys/Collections/common/Array"
    "~~/src/HOL/Imperative_HOL/Ref" (* where Ref imports Array*)

or this:

    "~~/src/HOL/Imperative_HOL/Array"
    "afp/thys/Collections/common/ArrayHashMap_Impl"

results in errors, as "Ref" uses the type "Heap.heap" and ArrayHashMap_Impl 
uses constant "Array.array_get".

Then, it is impossible to import "Collections" (importing "ArrayHashMap_Impl") 
and "Imperative_HOL" (importing "Ref") at the same time.

> So maybe a user-space workaround is an intermediate theory
> ...
> Would this solve your issue?

It would not solve the issue as the intermediate theory would have to be 
inserted in "Collections" or "Imperative_HOL" and it would then be easier to 
change one theory name.

I will try to import selectively theories "Ref" and "Mrec" of "Imperative_HOL" 
as I don't use "Imperative_HOL" arrays anyway... but I could have...

I hope to see soon localization of theories...

Thank you both,

Mathieu





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