[isabelle-dev] Semantics of hide (open)

[Florian Haftmann]

> I have the situation that I want to define via primrec a function with
> an existing popular name (append) but retain the commonplace accesses
> append for List.append and append.simps for List.append.simps (see
> attached theory for a contrieved example).  With the existing semantics
> of hide (open), I cannot achieve the desired effect; either (with
> (open)), append.simps remains shadowed, or (without (open)) I am not
> able to access Thy.append.simps any longer.
> 
> Maybe there is some confusion what the semantics of hide (open) is
> exactly supposed to be.  But since the current state of affairs gives no
> tool at hand to resolve situations as sketched above, this is a serious
> obstacle.

An appendix: the corresponding code is in name_space.ML

> fold (del_name name)
>   (if fully then names else inter (op =) [Long_Name.base_name name] names)

i.e. it delete all accesses except qualified ones.  This seems to be
deep-rooted in history (and is also documented in the Isar reference
manual).  Nevertheless I ask why not all accesses except the authentic
one (= name) are deleted.

	Florian

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 261 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20121228/4aa3f997/attachment.sig>