对集合进行过滤

Question

我正在处理集合的集合，其中内部集合是对象的表示，即内部集合的元素是形式对（属性，值）。

在一个简化的玩具示例中，我有两个属性，make（具有三个值）和engine（具有两个值）。给定一组这样的“对象”，

D

（例如汽车经销商库存），我希望能够过滤具有 V6 发动机的品牌集。

到目前为止，我所做的就是以

D

的形式返回具有 V6 的

v6s

的子集。显然，这给了我一组对

{(toyota, v6), (chevy, v6)}

。

我如何进一步过滤这一点？我需要某种

v6make :: "pair set" where "v6make = ???"

将会返回

{toyota, chevy}

type_synonym pair = "nat × nat"

definition make :: nat where "make = 1"
definition engine :: nat where "engine = 2"

definition toyota :: pair where "toyota = (make, 1)"
definition ford :: pair where "ford = (make, 2)"
definition chevy :: pair where "chevy = (make, 3)"

definition v4 :: pair where "v4 = (engine, 4)"
definition v6 :: pair where "v6 = (engine, 6)"

definition D :: "pair set set" where 
  "D = {{toyota, v6}, {ford, v4}, {chevy, v4}, {chevy, v6}}"

definition v4s :: "pair set set" where "v4s = Set.filter (λx. v4 ∈ x) D"
definition v6s :: "pair set set" where "v6s = Set.filter (λx. v6 ∈ x) D"

Answer 1

我找到了一个解决方案：D

definition v4make :: "pair set" where 
  "v4make = Set.filter (λx. fst x = make) (⋃{x. x ∈ v4s})"

还有更好的吗？