[isabelle-dev] adhoc overloading: order inserting overloaded constant

[Christian Sternagel]

Dear all,

recently I was working a lot with adhoc_overloading. Doing so I often 
experienced that my output differed from my input (w.r.t. adhoc 
overloading). At that time I did not think too much about it since being 
able to input readable formulas was quite enough. But today I suddenly 
had an idea what could cause this (to me) strange behavior.

First a minimal example. I introduce a new constant that will be overloaded.

   consts F :: "'a ⇒ 'a" ("FOO")

Then I add a locale and register its fixed constant for adhoc overlaoding:

   locale a =
     fixes f :: "'a ⇒ 'a"
     assumes nothing: "f x ≡ x"
   begin

   adhoc_overloading
     F f

   end

Inside this locale I can enter "FOO" instead of "f" and "f" will be 
printed as "FOO", as I would expect.

Now lets introduce another locale that is built on top of the first one

   locale set_a =
     elt: a elt_f for elt_f :: "'a ⇒ 'a"
   begin

   adhoc_overloading
     F elt_f

   definition "set_f A = elt_f ` A"

   adhoc_overloading
     F set_f

We now have adhoc overloading for elt_f as well as set_f. For inputting 
terms this works as I would expect (i.e., I get an error if it is not 
clear from the type which of elt_f and set_f should be inserted for any 
given FOO and the corresponding constant, otherwise).

However, as output for

   term "A (FOO {x. True})"

I obtain

   "A (set_a.set_f FOO {x. True})"

while I would have liked to get

   "A (FOO {x. True})"

since this is more readable. Looking at the code of "insert_overloaded" 
inside adhoc_overloading.ML reveals a use of "Pattern.rewrite_term", 
which seems to do bottom-up rewriting.

So my idea was to instead use top-down rewriting (i.e., first replace 
maximal subterms that fit a given pattern). This is what 
"Pattern.rewrite_term_top" does, right? So after replacing 
"rewrite_term" by "rewrite_term_top", I get the expected results.

Now my question. Can anybody think of a reason why "rewrite_term_top" 
would not be generally preferable over "rewrite_term" inside of 
"insert_overloaded"?

If not, could one of the devs incorporate this tiny change please?

cheers

chris