recursion - 如何在 Isabelle/HOL 中定义递归函数？

Question

如图，这是一个代码示例，定义了模型转换中源模型和目标模型的数据类型和有趣的功能。前三张图分别对应源模型架构、目标模型架构，以及它们之间的转换关系。最后三张图的递归函数的含义：

图4中定义的函数Part1是基于几个递归函数（如getPlaces等）

图 5 中定义的函数 Part2 基于几个递归函数。（如getTranStep2等）

图6是上面的基本递归函数getPlaces，描述了接收源模型SMD中Allstate列表的参数（包括最终状态、简单状态、复合状态），并返回places，但不考虑SMD初始状态。

最后三张图中递归函数的表达式看不懂，尤其是链接表达式的字符（'''''、[]、@、#、LL、st、substs），让我无法理解如何递归函数表达的意思。

其实我只是想定义我的源模型和目标模型。（比如左边三个元素对应右边一个元素；左边一个元素对应右边两个元素）

Answer 1

好吧，@只是列表连接，x # xs是带有 headx和剩余列表的列表xs，''''是空字符串，例如，''hello''将是字符串“hello”，请注意字符串只不过是字符列表。和ll只是st变量。

如果您在理解这些基本部分时遇到问题，我建议您先阅读一些关于 Isabelle 的一般性介绍，例如，通过开始isabelle doc prog-prove或阅读“具体语义”一书。