问题标签 [isabelle]

此外，Isar 还具有在 Isar 证明块中引入事实assume的命令。presume从我在文档中看到和阅读的内容来看，它不需要在目标中明确列出假设（假设？），并且似乎添加了一个案例来表明假设的陈述遵循其他目标。

所以问题是：我什么时候用presume代替assume，我可以用什么好技巧presume？

很多时候我遇到的问题是sledgehammer找到一个证明，但是当我插入它时，它并没有终止。我想sledgehammer这是 Isabelle 最重要的部分之一，但如果证明失败，它会变得很烦人。

在Sledgehammer 教程中，有一个小章节是“为什么 Metis 无法重构证明？”。

它列出：

1. 尝试isar_proofs获取逐步 Isar 证明的选项，其中每一步都由metis. 由于步骤相当小， metis因此更有可能重播它们。
2. 尝试smt证明方法而不是metis. 它通常更强大，但您需要有 Z3 可用于重放证明、信任 SMT 求解器或使用证书。
3. 尝试blastor autoproof 方法，根据需要通过unfolding, using, intro:, elim:, dest:, 或传递必要的事实simp:。

问题是第一个选项使证明更加冗长，并且还涉及人工干预。第二个选项很少奏效。

那么第三个选项呢。我可以应用任何易于遵循的启发式方法吗？

unfolding和有什么区别using？还有关于如何使用intro:,elim:和dest:来自失败metis证明的最佳实践吗？

部分示例

我想去掉证明的第一行，因为这行似乎微不足道。如果我删除第一行，sledgehammer仍然会找到一个证明，但是这个找到的证明失败（不会终止）。

我最近开始使用伊莎贝尔定理证明器。因为我想证明另一个引理，所以我想使用与引理“det_linear_row_setsum”中使用的符号不同的符号，它可以在 HOL 库中找到。更具体地说，我想使用“χ ij notation”而不是“χ i”。一段时间以来，我一直在尝试制定一个等效的表达式，但还没有弄清楚。

..

我有一个 Isabelle 理论文件，名为John.thy. 我想把它展示给我的朋友，但我的朋友没有 Isabelle，而且原始.thy文件不太容易阅读。我在 Isabelle 库中看到了一些网页（例如：http: //isabelle.in.tum.de/library/HOL/Finite_Set.html），它们具有漂亮的语法突出显示，我希望我的理论看起来像那样。

那么我该怎么做John.html呢？我查看了文档，所有的构建文件和制作文件等看起来都相当可怕和困难。某个善良的灵魂可以解释最简单的方法吗？

我创建了一个名为 的记录类型graph，并定义了一个合适的“是”关系的子图。我想表明一组图与子图关系形成一个顺序，即是ord类的一个实例。但我无法让它工作。这是我的最小工作示例：

我得到错误：

Type unification failed: No type arity graph_ext :: ord"

我尝试输入诸如instantiation graph :: ordand之类的内容instantiation graph_ext :: ord，但似乎没有任何效果。有任何想法吗？

我希望为 Isabelle 理论（例如 HOL 会话）生成 HTML 文档，但不包括证明。

也就是说，我想制作像http://isabelle.in.tum.de/library/HOL/Nat.html这样的页面 ，而不是，例如，

我只想看

原因是我使用 HTML 页面来查看可用的定理，但在这种情况下，证明只会分散注意力。（我知道在生成 PDF 时可以省略证明，但我对 HTML 文档特别感兴趣。）

我想在自然数向量中找到最大值。然而，Vector（即'vec'）是与Set 或List 不同的类型。我想了几个不起作用的想法，比如调平或提升 vec 的类型或递归函数的定义。

你建议什么解决方案来获得向量中的最大值？

我试图证明以下含义：

我认为这将是相当微不足道的，这就是为什么我尝试使用大锤来证明。不幸的是，这失败了。要么我的定义是错误的，要么涉及像 Max 这样的大运营商的自动证明存在一些困难。

我试图通过查看它们的定义以及我能找到的任何文档来更好地理解 Max 和 max。正如我之前遇到过 Isabelle 的一个问题，尽管它看起来微不足道（“为什么 Isabelle 不简化我的“if _ then _ else”构造的主体？ ”），但最终结果证明它需要大量经验，我决定在这里发布这个问题。

有时<statement> solve_direct（我通常通过 调用<statement> try）列出许多库定理并说“当前目标可以直接解决：……”。

设<theorem>为 的一个搜索结果solve_direct，那么在大多数情况下我都可以证明<statement> by (rule theorem)。

但是，有时这样的证明不被接受，导致错误消息“无法应用初始证明方法”。

是否有一种通用的、不同的技术来重用由 找到的定理solve_direct？

还是取决于个人情况？我可以尝试制定一个最小的示例并将其附加到这个问题上。

Isabelle has a quick_and_dirty mode that allows proofs to be skipped with sorry. It is enabled by default in jEdit and disabled by default with isabelle build. How can I change the setting

• In jEdit (interactively or with a command line parameter),
• For isabelle build, from the command line,
• For isabelle build, in the ROOT file, respectively.

Also, are there other means of asking Isabelle, preferably interactively in jEdit, “What lemmas in the current theory and its parents have been proven using a sorry“?

(I am asking this here in the hope that there will always be up-to-date-answers, in contrast to some mailing list posts that I find with google.)