Christian Sternagel wrote:

and after proving lemmas using e.g., Sp, I can transform them to lemmas
for S using the attribute [to_set] as in,
lemma refl: "Sp x x" by simp
lemma "(x,x) : S" using refl[to_set] .

Hi,
note that inductive_set already proves both the set and the predicate version
of the intro, cases, and induct rules for you, so there is no need to prove
them manually. For example, if you define

inductive_set S :: "('a * 'a)set" where refl: "(x,x) : S"
you get the following theorems:
S.refl: (x, x) : S
Sp.refl: S x x
S.induct: [| (x1, x2) : S; !!x. P x x |] ==> P x1 x2
Sp.induct: [| Sp x1 x2; !!x. P x x |] ==> P x1 x2
The [to_set] attribute and the inverse [to_pred] attribute are only needed
for transforming more complex theorems that have been derived from the above
primitive rules (as it is done e.g. in HOL/Transitive_Closure.thy).

So far so good. However, I was not able to find a method to directly
transform facts like `(a,b) : S` into `Sp a b` and vice versa.

What exactly do you mean by "directly"? I could not think of a more
"direct" way than the application of an attribute.

to me why do you need both the set and the predicate version of your
definition in the same theory. It might be easier to stick to a particular
notation, e.g. the predicate notation, which is usually more lightweight.
Greetings,
Stefan