Как определить рекурсивную функцию в Isabelle / HOL?

Question

Как показано на рисунке, это пример кода, который определяет типы данных и забавные функции исходной и целевой моделей в преобразовании модели. Первые три рисунка соответствуют архитектуре исходной модели, архитектуре целевой модели и взаимосвязи преобразования между ними. Значение рекурсивной функции последних трех изображений:

Функция Part1, определенная на рисунке 4, основана на нескольких рекурсивных функциях. (Таких как getPlaces, et c.)

Функция Part2, определенная на рисунке 5, основана на нескольких рекурсивных функциях. (например, getTranStep2, et c.)

Рисунок 6 - это базовая c рекурсивная функция getPlaces, которая описывает параметры списка Allstate (включая конечное состояние, простое состояние, составное состояние) в принимающая исходная модель SMD, и возвращает места, но не учитывает начальное состояние SMD.

Я не понимаю выражение рекурсивной функции на последних трех изображениях, особенно символы выражения ссылки ( '' '', [], @, #, LL, st, substs), что мешает мне понять, как рекурсивная функция выражает смысл.

Фактически, я просто хочу определить свою исходную модель и целевая модель. (например, три элемента слева соответствуют одному элементу справа; один элемент слева соответствует двум элементам справа)

Answer 1

Ну, @ - это просто конкатенация списков, x # xs - это список с заголовком x и оставшимся списком xs, '''' - это пустая строка, например, ''hello'' будет строкой «привет "и обратите внимание, что строки - это не что иное, как списки символов. А ll и st - это просто переменные.

Если у вас есть проблемы с пониманием этих c частей, я предлагаю сначала прочитать общее введение в Изабель, например, начав isabelle doc prog-prove или читая книгу «Конкретная семантика».