问题标签 [isabelle]

我正在寻找一种工具（首选 GUI，但 CLI 可以），它允许我输入数学表达式，然后对它们执行操作，但将我限制为仅在数学上有效的操作。此外，该工具必须能够保存会话并稍后证明给定的一组已保存操作是有效的。

注意：我不是在寻找生成证明的系统，只是检查我手动指定的步骤是否有效。

我已经将ACL2用于类似的操作，并且在某些情况下效果很好，但在其他所有情况下都很难使用。

这个小项目是我的动力。它是一种 D 模板类型，允许求解方程。给定这个等式：

任何一个符号都可以设置为未知，并且评估该表达式将导致对该变量的赋值。它的工作原理是将表达式树构建到类型中，然后使用重写规则将其转换为可以为未知类型触发的东西。

我需要的是某种方法来验证重写规则。它们可以通过测试一个断言来验证，即给定一些关系是真的，另一个也是真的。

我想在名为 的理论中定义我自己的列表类型List，但已经有一个具有该名称的理论。有比 更轻量级的理论Main吗？

如何在 Isabelle 中应用案例分析？我正在寻找类似于apply (induct x)（用于归纳）的东西。

是否可以为使用案例分析或归纳时生成的变量起自己的名字？

如何在 Isabelle 的一组数字 (nat) 中找到最大元素。max 函数不起作用，因为它只定义为取两个元素中的最大值。我知道如何使用类似 reduce 的函数来实现它，但我不知道如何从一组中选择一个随机元素。

问题

Isabelle/HOL验证器的核心算法是什么？

我正在寻找计划元循环评估器级别的东西。

澄清

我只对Verifier感兴趣，而不是自动定理证明的策略。

语境

我想从头开始实现一个简单的证明验证器（纯粹是出于教育原因，而不是用于生产用途。）

我想了解 Isabelle/HOL 的核心Verifier算法。我不关心用于自动定理证明的策略/代码。

我怀疑核心验证器算法非常简单（而且优雅）。但是，我找不到它。

谢谢！

当我在Isabelle中陈述引理时，我经常输入nitpick，如果这没有给我一个反例。然后我键入sledgehammer以尝试自动查找证明。

我想知道：是否可以调用Nitpick和Sledgehammer以便它们同时运行？既然Sledgehammer已经将我的引理发送给了一堆自动证明者，那么这些证明者中的一个难道不能成为像Nitpick这样的反例发现者吗？

在 Isabelle 理论文件中，我可以编写简单的单行策略，例如：

然而，我发现，当我开始编写 ML 代码来自动化证明、生成 MLtactic对象时，这些单行代码变得相当冗长：

有没有更简单的方法可以在 Isabelle/ML 级别编写简单的单线战术？

例如，类似反引号：@{tactic "clarsimp simp: split_def split: prod.splits"}产生类型的函数context -> tactic，将是一个理想的解决方案。

对于AFP条目Dijkstra's Shortest Path Algorithm，证明大纲和证明文件都不存在 *。不幸的是，我没有找到在IsaMakefile本地构建这些文档的方法。获取这些文件的最佳方式是什么？

另一个问题，由于Dijkstra.thy依赖于许多其他理论，有没有办法更快地加载所有内容？

*)现在已修复。

我有一个foo适用于该string类型的函数。当我export_code foo in Scala file -得到一个非常丑陋的 Scala 代码时。

一个很长的列表，看起来像这样被创建