Re: [isabelle] A special notation for function application

Dear Jesus,

do you need your notation only as input syntax or do you want Isabelle to print function application this way, too? If it is for input only, you just have to restrict your abbreviation to the input parser and it works fine:

abbreviation (input)
   app :: "('b =>  'a) =>  'b =>  'a" ("<(_),(_)>" 90)
   where "<f, x> == f x"

term "<f, x>"

Without the (input) restriction, Isabelle's pretty printer loops when it tries to display the term again. I do not recommend that you use such syntax translations for output, because such a translation would apply to all function applications, which is probably not what you want. You could, however, restrict your translation to certain type classes (e.g., arbitrary functions from vector spaces to vector spaces). Still, you will have to install your own print translation to guarantee termination of the pretty printer.

By the way, any notation that works for "f x" also works for "[x, f]" even "[x, f]" is a proper constant instead of an abbreviation.

Hope this helps,

Am 04.08.2011 13:55, schrieb Jesus Aransay:
Dear all,

I was trying to introduce some additional notation for linear
functionals in vector spaces; the idea is to use:

"[x, f]" as an alternative notation for "f x", where "f" is a linear
functional (let's say, type "'a =>  'b") and "x" is an element of type
"'a" (note that the arguments f and x are interchanged in the proposed

I would like that all notation available for "f x" would still work
for the new notation "[x, f]", in such a way that

[x, f] \oplus [y, f]

would be equivalent to (without unfolding any particular definition):

f x \oplus f y

Is it possible to reach these behavior? How? Maybe brackets are
already a bit overloaded in terms of notation (lists, propositions...)
so a notation based for instance in "<x, f>" would be also

I tried the following approach (which does not interchange arguments)

   app :: "('b =>  'a) =>  'b =>  'a" ("<(_),(_)>" 90)
   where "<f, x>  == f x"

but then when I write, for instance, "term<f, x>" the system does not
seem to find the correct type of the expression.

Thanks for any hint,


Karlsruher Institut für Technologie
IPD Snelting

Andreas Lochbihler
wissenschaftlicher Mitarbeiter
Adenauerring 20a, Geb. 50.41, Raum 031
76131 Karlsruhe

Telefon: +49 721 608-47399
Fax: +49 721 608-48457
E-Mail: andreas.lochbihler at
KIT - Universität des Landes Baden-Württemberg und nationales Forschungszentrum in der Helmholtz-Gemeinschaft

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.