问题标签 [isabelle]

我想用来从 Isabelle文件isabelle build -D xxx中生成 LaTeX文件。但是Isabelle检查了所有的理论依赖，所有的相关文件都必须涉及。.tex.thy.thy

是否有可能我随便使用.thy有语法错误的文件来生成.tex文件？事实上，我只需要其中的一部分来写一篇论文。

我正在尝试使用传输包为自定义数据类型建立归纳规则，但apply transfer对我不起作用。这是一个简单的例子：

这个时候目标还是

并不是

我会期待的。在证明它之前我需要做什么来转移引理？

另外，一般来说，如何才能更好地控制apply transfer，或者至少是更好的调试方式？

我有这个 C 代码：

我想证明，不管列表有多长，当这个循环结束时，p->nextequalsNULL和 EIP 指的是这个循环之后的下一条指令。

但我不能。有谁知道如何证明Isabelle/HOL中的循环？

我正在为 Isabelle2013/HOL 寻找免费且高质量的教程和文档（除了在谷歌搜索和挖掘之后显而易见的教程和文档）。你能推荐一些吗？

我正在与图书馆合作HOL/Library/Polynomial.thy。

一个简单的属性不起作用。例如，程度2x *2等于2x-

我如何证明引理（即，删除“对不起”）：

.

从曼努埃尔的回答中，我正在寻找的解决方案：

我已经尝试证明乐趣bubble_main是有序的，但似乎没有任何方法有效。有人可以帮我证明引理吗is_ordered (bubble_main L)？

我只是删除了我以前所有的引理，因为似乎没有一个可以帮助Isabelle找到证据。这是我的代码/理论：

Cartesian_Euclidean_Space在（HOL/Multivariate_Analysis 目录中）有一个矩阵乘法定义：

现在平方矩阵将是A ** A和 A^3 将是A ** A ** A。

我找不到要定义的幂函数A^n （即A ** A ** ... ** An 次）。

库中是否有幂函数？需要手动定义吗？

梅蒂斯给了我警告：

这个警告是什么意思？这是否表明metis证明比没有警告时“不那么健全”？

我想A /\ B /\ C /\ D /\ E /\ F在伊莎贝尔身上证明。如何在 中自动将子目标拆分为 6 个单独的子目标proof(rule ...)，然后我可以分别证明它们？

当然，我可以写proof(rule conjI)5 次，但也许有更优雅的方式来一步拆分？

我对证明感到困惑

在伊莎贝尔。显然你可以

但是我如何使用规则来证明这一点？

或者，有没有办法转储simp使用的规则？谢谢。