"Double loop"集合理解

Question

我知道我错过了一些明显的东西，但我迷失在如何使这一个工作。我试图写出一种"笛卡尔积"的集合理解。给定一个有限集合S的有限集合，我想构建一对的集合的集合，其中每一对由S中的一个集合和该集合中的一个值v给出;每个集合对应s中的每一个集合都有一对

基本上，给出(简单的)例子

definition s1 :: "nat set" where 
"s1 = {1, 2}"
definition s2 :: "nat set" where
"s2 = {4, 5}"
definition S :: "nat set set" where 
"S = {s1, s2}"
value "{{(s, v) | s. s ∈ S} | v. v ∈ s}"

我想评价成为{{({1,2},1),({4、5},4)},{{1,2},(1),({4、5},5)},{{1,2},(2),({4、5},4)},{{1,2},(2),({4、5},5)}}

相反，它的求值为(我意识到它应该是)

"(λu. {({1, 2}, u), ({4, 5}, u)}) ` s"
:: "(nat set × 'a) set set"

变量u被绑定到一个自由变量" "，我不知道如何有不同的"u"s和绑定每个U到其"关联">

s ∈ S 

谢谢你的指点。

Answer 1

简单的方法是避免这个问题，并将所有内容表示为集合上的图像:

value "(λv. (Pair v) ` S) ` S"

一般来说，有两种方法来做这类事情:让代码生成器工作或更好的方法，即调整定义，使它们更容易适应计算模型。