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.