Isabelle HOL定义顶点标签时succ函数Set.set参数报错如何解决

• 错误出在succ函数的返回类型声明部分：Isabelle 中的set类型构造器仅接受1个类型参数，你写的('v,'w) set传入了2个类型参数，不符合语法要求，因此触发了参数数量不匹配的报错。
• 你原本想要表达的是「由顶点ID'v和标签'w组成的二元组的集合」，对应的正确类型写法是('v × 'w) set。

record ('v,'w) graph =
  nodes :: "('v×'w) set"
  edges :: "(('v×'w) × ('v×'w)) set"

definition succ :: "('v,'w) graph ⇒ 'v ⇒ ('v × 'w) set"
  where "succ G v ≡ {(v',w). ((v,w),(v',w))∈edges G}"

你当前的succ定义逻辑隐含了一个前提：同一个顶点IDv对应的标签w是唯一的，如果你的业务场景中允许同一个v绑定不同的w，可以根据需求调整集合推导式的约束条件即可。

内容的提问来源于stack exchange，提问作者Eva