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

Question

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

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

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

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

最后三张图中递归函数的表达式看不懂，尤其是链接表达式的字符（''''，[]，@，#，LL，st，substs），妨碍我从了解递归函数如何表达含义。

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

Answer 1

好吧，@ 只是列表连接，x # xs 是带有头部 x 的列表，其余列表 xs，'''' 是空字符串，例如，''hello'' 将是字符串“hello " 并注意字符串只不过是字符列表。而ll 和st 只是变量。

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