问题标签 [isabelle]

有时，当我在写应用风格的证明时，我想要一种方法来修改证明方法 foo以

尝试foo第一个目标。如果它解决了目标，很好；如果没有解决，恢复到原始状态并失败。

这出现在以下代码中：

在进一步进行一些更改之后，对的调用simp将不再完全解决目标，然后这将循环。如果我可以指定类似的东西

或（替代建议的语法）

或（也许更好的语法）

它会停在这个脚本无法解决的第一个目标上。

假设我有一个目录isabelle_afp，其中存储了很多理论。该目录是一个库，我不打算更改其中的文件。我想加快 Isabelle/jEdit 的启动时间（默认情况下，isabelle_afp我当前理论所依赖的所有理论都重新处理）。

我怎样才能跳过这一步？系统手册告诉我构建一个持久堆映像。最简单的方法是什么？

我怎样才能告诉 Isabelle/jEdit 加载这个堆图像？

我想匹配并删除与l :: 'a list谓词匹配的那些元素P :: ('a => bool)

完成此类任务的最佳方法是什么？如何找到可能对我有帮助的现有功能？

我想创建一个以元组作为参数的定义。

但是，这不被接受。错误信息是

使用fun而不是definition工作，但这不是我想要的。以下表示法也有效，但有点难看：

在 a 中使用元组作为参数的最佳方法是definition什么？

假设我想展示以下引理

我得到目标

但是，我不需要B. 我怎样才能将我的目标转移到类似的东西上

我不想改变原来的lemma陈述，只是应用风格的当前目标。

我想inductive在locale. 如果没有locale一切正常：

但是，当我在 a 中尝试相同的操作时locale，它不起作用：

语言环境中的code_pred行返回以下错误：

根据codegen文档部分“7.3 语言环境和解释”，从语言环境导出代码有点棘手但可以实现。以下示例工作正常：

如何为具有多个参数的语言环境导出代码？鉴于以下情况locale：

我可以用

但我不能在定义中使用这种解释

它失败了

我很想locale直接从定义中生成代码，而不需要解释。例子：

实例化的假设MyTest是可执行的，我可以为它们生成代码

我可以定义一个函数来执行isInL任意的定义MyTest。

但是，代码导出失败：

为什么我想做这样的事情？我正在使用 alocale的上下文，valid_graph例如，这里是有限的。测试图表是否有效很容易。现在我想将我的图形算法的代码导出到 Scala 中。当然，代码应该在任意有效图上运行。

我正在考虑类似于这样的 Scala 类比：

考虑以下语言环境定义：

在 Isar 中，如果我尝试使用f或 lemma的定义f_pos，则语言环境假设和固定变量对我来说是隐藏的。例如，thm f_def f_pos返回：

正如预期的那样。

然而，如果我试图在 ML 中推理这些术语，“隐藏的”固定变量就会突然暴露出来。ML {* @{thm f_def} |> prop_of *}，例如，返回：

其中固定变量a成为函数的参数f。

有没有办法能够在 ML 的语言环境中工作，这样我就不会接触到这样的语言环境变量？

最近学习了如何在应用式证明中删除不需要的前提，我现在想知道如何删除不需要的变量。也就是说，假设我有目标

wherey没有出现在A,B或C中。如何将其转换为以下内容？