[isabelle-dev] adhoc overloading: ugly output

[Christian Sternagel]

Here is a related thread

 
https://www.mail-archive.com/isabelle-dev@mailbroy.informatik.tu-muenchen.de/msg04950.html

which was originated by myself ;) (how embarassing).

cheers

chris

On 01/16/2015 02:35 PM, Christian Sternagel wrote:
> Dear all,
>
> in Isabelle2014 as well as c7f6f01ede15 I noticed that the output when
> using adhoc overloading together with abbreviations is not optimal
> (maybe this was already discovered before but I forgot about it). Now,
> it turns out that the same issue (at least superficially it's the same,
> but maybe caused by different reasons) arises also for definitions in
> local theory contexts (or are those the same as mere abbreviations?).
>
> Let me illustrate what I'm talking about by the following example:
>
> theory Foo
> imports
>    Main
>    "~~/src/Tools/Adhoc_Overloading"
> begin
>
> consts SHARP :: "'a ⇒ 'b" ("♯")
>
> context
>    fixes shp :: "'a ⇒ 'a"
> begin
>
> adhoc_overloading
>    SHARP shp
>
> definition le_sharp (infix "≤⇩♯" 50)
> where
>    "xs ≤⇩♯ ys ≡ list_all2 (λx y. y = x ∨ y = ♯ x) xs ys"
>
> term "xs ≤⇩♯ ys"
> text ‹
>    Result in @{term "Foo.le_sharp ♯ xs ys"} instead of
>    more desirable @{term "xs ≤⇩♯ ys"}. (The same happens
>    when we turn the above definition into an abbreviation.)
> ›
>
> end
>
> text ‹
>    In the "global" theory this also happens, but only for
>    abbreviations, not for definitions.
> ›
>
> definition "shp = id"
>
> adhoc_overloading SHARP shp
>
> definition le_sharp' (infix "≤⇩♯" 50)
> where
>    "xs ≤⇩♯ ys ≡ list_all2 (λx y. y = x ∨ y = ♯ x) xs ys"
>
> term "xs ≤⇩♯ ys"
>
> end
>
> Unfortunately, at the moment I do not have time to look into adhoc
> overloading myself, but let this thread be a reminder. If anybody else
> can provide explanations/comments/solutions, please go ahead!
>
> cheers
>
> chris