Express a parametric abbreviation in Isabelle

Question

I want to abreviate the equivalence class of a point:

r `` {p}

to

[p]

What is the right way to this in Isabelle?

Answer 1

You can only do this in a context where r is fixed, e.g. an anonymous context or a locale:

context
  fixes r :: "('a × 'a) set"
begin

abbreviation foo ("⟨_⟩" 1000) where
  "⟨p⟩ ≡ r `` {p}"

I used chevrons instead of brackets here because brackets would clash with the syntax for lists, so it wou