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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
