set - 有一组对（set_pairs），我想创建一组（set_fsts）这些对的第一个元素。我怎样才能在伊莎贝尔做到这一点？

Question

有一组对（set_pairs），我想创建一组（set_fsts）这些对的第一个元素。我是按以下方式写的

定义 "set_fsts = {f . p ∈ set_piars ∧ fst p = f}" 但伊莎贝尔向我展示了这个错误消息：rhs "p" 上的额外变量

你能帮我解决这个问题吗？

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

你可以试试

set_fsts = {fst p . p ∈ set_piars}

这适用于 Isabelle/ZF，我不确定 Isabelle/HOL。