伊莎贝尔：如何使用矩阵

【问题标题】：Isabelle: how to work with matrices伊莎贝尔：如何使用矩阵
【发布时间】：2013-05-22 10:20:04
【问题描述】：

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

到目前为止，我发现的关于矩阵的唯一帮助是查看source code in the HOL library。

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

【问题讨论】：

【解决方案1】：

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

【讨论】：

但请注意，此 AFP 条目的目的是专门用于可执行性（即，您可以为所有矩阵运算生成实际的可执行代码）。出于这个原因，必须在所有证明中进行一些假设（例如关于维度），这在证明抽象属性时可能会有点烦人。