我的问题是关于伊莎贝尔定理证明器的证明过程。
我目前对模型变换正确性的研究工作感兴趣。但是，在正式化建模语言时遇到了问题。对于形式化建模语言(包括源元模型、目标元模型、变换本身(，但不确定定理证明者的证明机制。
我是否应该在编程模式下使用.thy后缀自行编码理论文件，然后在证明模式下运行它以获得正确性证明？Isabelle有许多编码领域，例如数据类型，常量，函数，定义，引理和定理。我是否应该单独编写这些代码以证明模型转换的正确性？
我不确定我是否正确理解了你的问题，但我会尝试回答其中的一部分。
但是，在正式化建模语言时遇到了问题。
您能否澄清您遇到了哪些问题，或者给出您想要形式化的建模语言的具体示例？
我是否应该在编程模式下使用.thy后缀自行编码理论文件，然后在证明模式下运行它以获得正确性证明？
伊莎贝尔没有单独的编程和验证模式。您可以在同一个.thy文件中混合使用函数定义和引理。
正确性的大多数方面都是在引理/定理中完成的，但即使你只是在 Isabelle 中定义了一个递归函数，你也已经得到了一些正确性保证：你需要证明你的定义是明确的。
Isabelle有许多编码领域，例如数据类型，常量，函数，定义，引理和定理。我是否应该单独编写这些代码以证明模型转换的正确性？
正如我上面所说，您不需要将它们分成不同的文件。 但是，一切都必须在伊莎贝尔中按顺序定义。 例如，如果你想证明一个函数的某些东西，那么这个函数必须在源代码中的引理之前定义。 如果函数适用于某些数据结构，则相应的类型定义必须位于函数之前。