Вы можете сделать это только в контексте, где r фиксирован, например, в анонимном контексте или в локали:
context
fixes r :: "('a × 'a) set"
begin
abbreviation foo ("⟨_⟩" 1000) where
"⟨p⟩ ≡ r `` {p}"
Я использовал шевроны вместо скобок, потому что в скобках будет sh с синтаксис для списков, так что это будет