Isabelle: How can I position fixed arguments in mixfix notation?

Say I have the following definition of a reflexive and transitive closure of a relation, where relations are represented by binary predicates:

inductive
  closure :: "(['a, 'a] ⇒ bool) ⇒ (['a, 'a] ⇒ bool)"
  for ℛ (infix "→" 50)
where
  gen:
    "x → y ⟹ closure (→) x y" |
  refl:
    "closure (→) x x" |
  trans:
    "⟦closure (→) x y; closure (→) y z⟧ ⟹ closure (→) x z"

I want to have a nicer syntax for applications of closure. Say I’d like to be able to write x *(→)* y for closure (→) x y. The problem is that the argument order in this notation doesn’t match the argument order of the function closure.

I thought that perhaps the use of \<index> could help. Unfortunately, the documentation of \<index> in the Isabelle/Isar Reference Manual is very terse, and I couldn’t really make sense of it. I played a bit with \<index> but didn’t find any workable solution.

What puzzled me was that apparently \<index> gets translated to ⇘some_index⇙, judging from some error messages I got. I tried to use ⇘ℛ⇙ to mark the position where the base relation should go, but this didn’t work either.

Solution

To switch the arguments, an abbreviation is the best choice. (syntax/translations works, too, but abbreviations should be preferred because they work in any context (locales, type classes, ...) and are type-checked.) Fortunately, inductive allows you to simultaneously declare abbreviations together with an inductive definition. The equations for the abbreviations have to come first. Here's how it works for your example:

inductive closure :: "(['a, 'a] ⇒ bool) ⇒ (['a, 'a] ⇒ bool)"
  and closure_syntax :: "['a, ['a, 'a] ⇒ bool, 'a] ⇒ bool" ("(_ ⇧*(_)⇧* _)" [999,0,999] 100)
  for ℛ (infix "→" 50)
  where
  "x ⇧*(→)⇧* y ≡ closure (→) x y"
| gen: "x → y ⟹ x ⇧*(→)⇧* y"
| refl: "x ⇧*(→)⇧* x"
| trans: "⟦x ⇧*(→)⇧* y; y ⇧*(→)⇧* z⟧ ⟹ x ⇧*(→)⇧* z"

The syntax element \<index> is rarely used nowadays, because locales achieve a similar effect and are usually more flexible. The point of \<index> is that you can declare a parameter as (structure) and this will then automatically be inserted whereever the parser sees \<index> in the syntax grammar. So it allows you to omit repeating the structure parameter, but locales usually work better.