Isabelle中如何实现映射像内列表拼接、集合并集操作

集合场景下你已经知道用⋃运算符做全域并集，列表场景下直接用Isabelle内置的concat函数即可，它的作用就是将'a list list类型的嵌套列表拍平为单层列表，和集合的⋃作用完全对应，针对不同的映射类型具体写法如下：

• 针对全函数映射p :: nat ⇒ string list
  如果你需要拼接指定有限下标范围内的所有列表，写法为concat (map p 下标集合)。比如你给出的示例映射，计算concat (map p {0,1})就能直接得到预期结果["0.0", "1.0", "1.1"]。

  注意：不要直接用UNIV作为下标集合，UNIV代表全体自然数的无限集合，会导致求值时无限遍历无法终止，实际使用时替换为你实际赋值的有限下标集即可。

• 针对偏函数映射p :: nat ⇀ string list
  偏函数自带定义域限制，不需要手动指定下标范围，直接取偏函数的值域拼接即可，写法为concat (map the (ran p))。其中ran p会取出p所有有定义位置对应的字符串列表，the会剥离偏函数返回值的Some包裹，最后用concat完成拼接。

操作对应速查 #

你提到的四类场景的标准写法可以直接对照下表使用：

你给出的第二个集合示例，用⋃x∈{0,1}. p x就能得到预期的{"0.0", "1.0", "1.1"}结果，和列表操作的逻辑完全对齐。

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