matrix - 伊莎贝尔：如何使用矩阵

Question

大约 2-3 周前，我开始学习定理证明者 Isabelle。我仍然是一个绝对的初学者，到目前为止，我一直在学习“Isabelle/HOL 中的编程和证明”教程。

到目前为止，我发现的关于矩阵的唯一帮助是查看HOL 库中的源代码。

现在我想学习如何证明矩阵的性质。矩阵的 lambda 语法对我来说仍然是新的。有没有关于在 Isabelle 中使用矩阵的教程或基本/中级示例？

Answer 1

这是法新社http://afp.sourceforge.net/entries/Matrix.shtml中更新的/最新条目

CeTA http://cl-informatik.uibk.ac.at/software/ceta/在这里被引用为一个应用程序，因此您可以在那里查看它在实践中如何使用的示例。