Re: [isabelle] Theory name conflict



> Making the name shorter will inevitably provoke new conflicts. If you
> change it, make it longer, e.g. Heap_Array. Users usually don't import
> this theory individually, only the via Imperative_HOL entry point.
> 
> But I now see that the theory name is intended as a qualifier for
> constants... Could one achieve this behavior using other means, e.g., a
> vacuous locale or something?

In principle, yes.  But it is a complication and cluttering, no
simplification.

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.

So maybe a user-space workaround is an intermediate theory

theory Heap_Array
imports "~~/src/HOL/Imperative_HOL/Array"
begin

lemmas xyz = Array.xyz

...

end

and then in the main theory the imports

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

which would allow to access the facts mirrored in Heap_Array by
Heap_Array.xyz.

Would this solve your issue?


Hope this helps,
	Florian

-- 

Home:
http://www.in.tum.de/~haftmann

PGP available:
http://home.informatik.tu-muenchen.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.