我的问题是关于Isabelle定理prover的证明过程。
我目前感兴趣的研究工作是在 模型转换的正确性. 但是，在形式化建模语言方面遇到了问题。对于形式化的建模语言（包括源元模型、目标元模型、转换本身），但它对 定理的证明机制.
我应该在编程模式下自编一个后缀为.thy的理论文件，然后在证明模式下运行，以获得正确性证明？Isabelle有很多编码字段，如数据类型、常量、函数、定义、稃和定理。我应该 分别编码 来证明模型变换的正确性？
我不确定我是否正确理解了你的问题，但我会尝试回答部分问题。
但是，在建模语言的形式化过程中遇到了问题。
能否说明一下你遇到了哪些问题，或者举一个具体的例子说明你要形式化的建模语言？
是否应该在编程模式下自编一个后缀为.thy的理论文件，然后在证明模式下运行，得到正确性证明？
Isabelle没有单独的编程模式和验证模式。你可以将函数定义和词法混合在同一个 .thy 文件。
正确性的大部分方面都是在 lemmastheorems 中完成的，但即使你只是在 Isabelle 中定义了一个递归函数，你也已经可以得到一些正确性的保证：你需要证明你的定义是定义好的。
Isabelle有很多编码字段，比如数据类型、常量、函数、定义、公理和定理。我是否应该分别对这些进行编码以证明模型转换的正确性？
正如我上面所说，你不需要把它们分开到不同的文件中。然而，所有的东西都必须在Isabelle中按顺序定义.例如，如果你想证明一个函数的一些东西，那么函数必须在源代码中的稃之前定义.如果函数在一些数据结构上工作，相应的类型定义必须在函数之前。