Isabelle：更改列表中的元素

Question

在VDM中，我们可以做如下的事情

someSequence(index) := someSequence(index) union {x}

其中 someSequence 是一组序列。

在 Isabelle 中，如何访问列表中的元素并像上面的示例那样修改它？有办法吗？

感谢您的帮助！

Answer 1

你说的是序列集，但你问的是列表。这是列表函数：

value "(list_update [1,2,3,4,5::nat] 2 0) = [1,2,0,4,5]"

有main.pdf，可以快速概览常见类型的函数和语法。第 9 页是列表概述：

我查看了函数签名，直到我看到它接受并返回了正确类型的参数。

他们是 Isabelle/HOL 逻辑的 PDF。第 66 章是他们为 Isabelle2015 定义列表的地方。新版本的页码和章节可能会更改。

在第 1033 页上，有一个他们执行的检查列表，作为一些常见列表函数的示例：

他们不试图使列表函数库详尽无遗。您可以使用他们所做的，作为如何定义您自己的示例。

Isabelle: changing an element inside a list