There is a set of pairs (set_pairs) and I want to create a set (set_fsts) of first elements of those pairs. How can I do this in Isabelle?

Question

There is a set of pairs (set_pairs) and I want to create a set (set_fsts) of first elements of those pairs. I am writing it in the following way

definition "set_fsts = {f . p ∈ set_piars ∧ fst p = f}" but Isabelle shows me this err msg: Extra variable on rhs "p"

Could you please help me with this?

Answer 1

You need to introduce p by existential quantification, i.e. EX p. P : set_pairs ...

Shorter way would be to define set_fsts as fst ` set_pairs

Answer 2

You can try

set_fsts = {fst p . p ∈ set_piars}

This would work in Isabelle/ZF, I am not sure about Isabelle/HOL.