使用Isabelle's theorem prover 证明的过程是在编程模式下编码，然后在证明模式下验证吗？
Is the process of proving using Isabelle's theorem prover coded in programming mode and then verified in proof mode?
我的问题是关于伊莎贝尔定理证明器的证明过程
我目前对 模型转换正确性 的研究工作很感兴趣。然而，在形式化建模语言时遇到了问题。对于形式化的建模语言（包括source meta-model，target meta-model，transformation本身），但是对于定理证明者的证明机制没有把握
我是否应该在编程模式下使用 .thy 后缀自编码理论文件，然后 运行 在证明模式下对其进行正确性证明？ Isabelle 有许多编码领域，例如数据类型、常量、函数、定义、引理和定理。我是否应该单独编码这些以证明模型转换的正确性？
我不确定我是否正确理解了你的问题，但我会尽力回答部分问题。
However, problems were encountered in formalizing the modeling language.
您能否说明您遇到了哪些问题或给出您想要形式化的建模语言的具体示例？
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 没有单独的编程模式和验证模式。您可以在同一 .thy 文件中混合使用函数定义和引理。
大多数方面的正确性都在 lemmas/theorems 中完成，但即使您只是在 Isabelle 中定义一个递归函数，您也已经获得了一些正确性保证：您需要证明您的定义是明确定义的。
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?
正如我上面所说，您不需要将它们分成不同的文件。
然而，一切都必须在 Isabelle 中按顺序定义。
例如，如果你想证明一个函数，那么函数必须在源代码中的引理之前定义。
如果该函数适用于某些数据结构，则相应的类型定义必须位于该函数之前。
我的问题是关于伊莎贝尔定理证明器的证明过程
我目前对 模型转换正确性 的研究工作很感兴趣。然而，在形式化建模语言时遇到了问题。对于形式化的建模语言（包括source meta-model，target meta-model，transformation本身），但是对于定理证明者的证明机制没有把握
我是否应该在编程模式下使用 .thy 后缀自编码理论文件，然后 运行 在证明模式下对其进行正确性证明？ Isabelle 有许多编码领域，例如数据类型、常量、函数、定义、引理和定理。我是否应该单独编码这些以证明模型转换的正确性？
我不确定我是否正确理解了你的问题，但我会尽力回答部分问题。
However, problems were encountered in formalizing the modeling language.
您能否说明您遇到了哪些问题或给出您想要形式化的建模语言的具体示例？
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 没有单独的编程模式和验证模式。您可以在同一 .thy 文件中混合使用函数定义和引理。
大多数方面的正确性都在 lemmas/theorems 中完成，但即使您只是在 Isabelle 中定义一个递归函数，您也已经获得了一些正确性保证：您需要证明您的定义是明确定义的。
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?
正如我上面所说，您不需要将它们分成不同的文件。 然而，一切都必须在 Isabelle 中按顺序定义。 例如，如果你想证明一个函数，那么函数必须在源代码中的引理之前定义。 如果该函数适用于某些数据结构，则相应的类型定义必须位于该函数之前。