如何在Isabelle/HOL中从含V6引擎的集合的集合提取品牌集合？

我正在处理集合的集合，内层集合用来表示对象，每个内层集合的元素都是(属性, 值)形式的pair。
简化场景里有两个属性：make（有3个取值）和engine（有2个取值）。给定这类“对象”的集合D（比如汽车经销商库存），我要筛选出配备V6引擎的品牌集合。
目前我只能通过v6s得到D中包含V6的子集，形式是{{toyota, v6}, {chevy, v6}}这样的pair集合的集合。
我该怎么进一步过滤？需要定义类似v6make :: "pair set" where "v6make = ???"的表达式，让它返回{toyota, chevy}。

相关Isabelle/HOL代码 #

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"

解决方案 #

要提取配备V6引擎的品牌，可通过遍历v6s中的对象集合，筛选出每个集合里属性为make的pair，最终合并为目标集合。以下是两种可行的定义方式：

方式1：集合推导式 #

definition v6make :: "pair set" where
  "v6make = { p | p x. x ∈ v6s ∧ p ∈ x ∧ fst p = make }"

方式2：集合并运算结合筛选 #

definition v6make :: "pair set" where
  "v6make = ⋃x∈v6s. { p ∈ x | fst p = make }"

说明 #

• 集合推导式：遍历v6s中的每个对象集合x，从中取出所有满足fst p = make的pairp，将这些pair收集为最终集合。
• 集合并运算：对v6s里的每个x，先筛选出x中属性为make的pair，再将所有筛选后的子集合并为一个大集合。

两种方式都会从{{toyota, v6}, {chevy, v6}}中提取出toyota和chevy，最终得到目标集合{toyota, chevy}。

内容的提问来源于stack exchange，提问作者Alicia M.