[isabelle-dev] [isabelle] Good name for "sublist" predicates

[Makarius]

On 30/06/17 16:39, Manuel Eberl wrote:
> 
> The advantage of qualified names is that they really allow us to add
> disambiguating context to ambiguous names when necessary, e.g. something
> like "List.subseq" and "Topological_Spaces.subseq". Still, as I said, I
> do understand that typing such lengthy names is tedious.

Just for typing it there is semantic completion in the Prover IDE. For
constants in the term language, it requires trailing "_" to say that it
is really meant to be a constant and not a variable.

To actually complete such long name components as "subseq" in
"Topological_Spaces.subseq", I have now made a tiny change in
Isabelle/f50e6e31a0ee. Also note that the completion history reorders
frequently used completions later on, so the long list of completion
items becomes practically usable.


> Incidentally, I wonder if it is possible to locally prefer one of the
> two constants, i.e. say that, in the following block, I want "subseq" to
> mean "Topological_Spaces.subseq". That might also mitigate the problem
> of long qualified names.

That introduces some extra complexity in the theory source, apart from
input methods. Nonetheless, the 'alias' command from
Isabelle/df85956228c2 can in principle do that: it merely exposes an
important Isabelle/ML interface from recent years as Isar command.

I did not do this earlier, because aliases have the potential for extra
confusion of names in a theory, but proper name space operations are
better than simulating that with 'notation' / 'no_notation'. (Alphabetic
syntax tokens should be kept at a minimum anyway: they are subtracted
from the identifier syntax category.)


	Makarius