How to define a recursive function in Isabelle/HOL?

Question

As shown in the figure, this is a code example that defines the data types and fun functions of the source and target models in the model transformation. The first three figures correspond to the source model architecture, target model architecture, and the transformation relationship between them. The meaning of the recursive function of the last three pictures:

The function Part1 defined in Figure 4 is based on several recursive functions.(such as getPlaces, etc.)

The function Part2 defined in Figure 5 is based on several recursive functions. (such as getTranStep2, etc.)

Figure 6 is the above basic recursive function getPlaces, which describes the parameters of the Allstate list (including final state, simple state, composite state) in the receiving source model SMD, and returns places, but does not consider the SMD initial state.

I don’t understand the expression of the recursive function in the last three pictures, especially the characters of the link expression (' ' ' ', [ ], @, #, LL, st, substs), which prevents me from understanding how the recursive function expresses the meaning.

In fact, I just want to define my source model and target model. (for example, three elements on the left correspond to one element on the right; one element on the left corresponds to two elements on the right)

Answer 1

Well, @ is just list concatenation, x # xs is the list with head x and remaining list xs, '''' is the empty string, e.g., ''hello'' would be the string "hello" and note that strings are nothing else than lists of characters. And ll and st are just variables.

If you have problems understanding these basic parts, I suggest to first read some general introduction to Isabelle, e.g., by starting isabelle doc prog-prove or by reading the book "Concrete Semantics".