My question is about the proof process of the Isabelle theorem prover.
I am currently interested in research work on the correctness of model transformations. However, problems were encountered in formalizing the modeling language. For the formal modeling language (including source meta-model, target meta-model, transformation itself), but it is not sure about the proof mechanism of the theorem prover.
Should I self-code a theory file with .thy suffix in programming mode, and then run it in proof mode to get a proof of correctness? Isabelle has many coding fields, such as data types, constants, functions, definitions, lemmas and theorems. Should I code these separately to prove the correctness of the model transformations?
I am not sure I understand your question correctly, but I will try to answer parts of it.
However, problems were encountered in formalizing the modeling language.
Could you clarify which problems you encountered or give a concrete example of the modelling language you want to formalize?
Should I self-code a theory file with .thy suffix in programming mode, and then run it in proof mode to get a proof of correctness?
Isabelle does not have separate modes for programming and for verification. You can mix function definitions and lemmas in the same .thy file.
Most aspects of correctness are done in lemmas/theorems, but even if you just define a recursive function in Isabelle you will already get some correctness guarantees: you need to prove that your definition is well-defined.
Isabelle has many coding fields, such as data types, constants, functions, definitions, lemmas and theorems. Should I code these separately to prove the correctness of the model transformations?
As I said above you don't need to separate them into different files. However, everything must be defined in order in Isabelle. For example if you want to prove something about a function, then the function must be defined before the lemma in the source code. If the function works on some data structure, the corresponding type definitions have to come before the function.