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

Question

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

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

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

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

我不了解最后三张图片中递归函数的表达式，尤其是链接表达式的字符（''''，[]，@，＃，LL，st，substs），这使我无法了解递归函数如何表达含义。

实际上，我只想定义我的源模型和目标模型。 （例如，左侧的三个元素对应于右侧的一个元素；左侧的一个元素对应于右侧的两个元素）

Answer 1

[嗯，@只是列表串联，x # xs是头为x，其余列表为xs的列表，''''是空字符串，例如，''hello''将是字符串“ hello”请注意，字符串不过是字符列表而已。 ll和st只是变量。

[如果您在理解这些基本部分时遇到困难，我建议首先阅读Isabelle的一般介绍，例如，通过开始isabelle doc prog-prove或阅读《具体语义学》。