Linked Questions

Popular Questions

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

Asked by At

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.

Related Questions