It is amazing how easy some things get when a wizard is looking over
your shoulder (thanks Florian!). It turns out that adhoc overloading
(which is in essence very similar to abbreviations) did not observe some
conventions that are followed by the "abbreviation" command.
By peeking into the sources - even without understanding much of it ;) -
it can be seen that the flag "abbrev_mode" is checked for abbreviations.
By doing the same inside "adhoc_overloading" the ugly output I presented
earlier, turned into beautiful symbols.
Could one of the developers be so kind to apply the attached (mq) patch
(after testing it of course) ;) ?
cheers
chris
On 01/16/2015 02:40 PM, Christian Sternagel wrote:
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
# HG changeset patch
# Parent 4427f04fca57ea90f7fd8dbc271ac29a9268ec75
adhoc overloading must follow the same conventions as abbreviations
diff -r 4427f04fca57 -r fbefd978e72d src/Tools/adhoc_overloading.ML
--- a/src/Tools/adhoc_overloading.ML Sun Jan 25 22:11:06 2015 +0100
+++ b/src/Tools/adhoc_overloading.ML Tue Jan 27 13:59:16 2015 +0100
@@ -179,7 +179,9 @@
map (fn t => Term.map_aterms (insert_variants ctxt t) t);
fun uncheck ctxt ts =
- if Config.get ctxt show_variants orelse exists (is_none o try Term.type_of)
ts then ts
+ if Proof_Context.abbrev_mode ctxt orelse
+ Config.get ctxt show_variants orelse
+ exists (can Term.type_of) ts then ts
else map (insert_overloaded ctxt) ts;
fun reject_unresolved ctxt =
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
