问题标签 [hol]

是否可以在 Isabelle/HOL 中编写递归 lambda 表达式？如果是这样，怎么做？

例如（一个愚蠢的）：

所以不是......我想编写应用于 x-1 的 λ 函数。

我该怎么做？提前致谢。

我正在尝试为此功能提供自动终止证明：

isEmpty存在_

我对此完全陌生，所以我不知道终止证明是如何工作的，或者 pat_completeness 是如何工作的。

任何人都可以提供参考以了解更多信息和/或帮助我解决这个特定的例子吗？

提前致谢。

我在学习伊莎贝尔的展开规则时遇到了一些问题。希望有人能解答，谢谢。

1. 我需要导入 Isabella 的内置 HOL 库来引入一些已定义的量词。当我用Isabella2017打开%ISABELLE_HOME%\src\HOL\HOL.thy时，第七行“theory HOL”会报错“Cannot update finished theory"HOL.HOL"”。

2. 你遇到过同样的问题吗？您是如何在 HOL 库中引入内置规则的？

在证明几个引理时，我发现了同样的问题：具有相等性的规则有时只在一个方向上起作用。

例如，我想使用append_assocto get from xs @ ys @ zsto (xs @ ys) @ zs，但由于append_assoc定义为(xs @ ys) @ zs = xs @ ys @ zs，我不能。

有什么方法可以表明我想向后使用一些规则？

提前致谢。

我已经与 Isabelle/HOL 合作了几个月，但我一直无法弄清楚使用_tac的确切意图。

具体来说，我说的是case与case_tac和induct与indut_tac （尽管一般来说了解tac的含义会很好，因为我也在使用其他方法，例如cut_tac）。

我注意到我不能使用带有 ⋀ 绑定变量的 apply 来使用案例或归纳，但如果它是结构化证明，我可以。为什么？

一个例子：

另一方面，我注意到 induct 和 induct_tac 之间的另一个区别是我可以对后者使用双重感应，但不能对前者使用。再说一次，我不知道为什么。

提前致谢。

我正在尝试在 Isabelle HOL 中定义一些顶点标签，并且后继定义存在问题：

它说“类型构造函数的参数数量错误：“Set.set””，有人知道如何解决这个问题吗？

我试图从上一个问题中证明 Isabelle (2021) 中的以下推理规则：

特别是，我试图以向前的方式证明这一点，首先使用两个假设来获得A(y)和B(y)，因此A(y) /\ B(y)，对于任意选择的y。但是，我无法弄清楚∀在最后一步中引入背面的正确方法是什么，如下面的问题行所示。

有人可以帮助解释什么是正确的假设方法，然后在这里抽象出任意变量y吗？

我开始使用 Isabelle HOL，并想尝试构建某种组合证明。我一开始就采用了 Cayley 的公式。

这里是： 对于每个正整数 n，n 个标记顶点上的树数为 n^{n-2}。

在伊莎贝尔身上怎么会这样？我假设我必须定义树，但那又如何呢？

任何帮助或相关文章和/或代码将不胜感激！提前致谢

有一组一些结构。我试图证明集合的基数等于某个数字。完整的理论太长，无法在此处发布。所以这里是一个简化的，只是为了展示这个想法。

让对象（我需要计算）是包含从 1 到 n 的自然数的集合。证明思路如下。我定义了一个函数，它将集合转换为 0 和 1 的列表。这是函数及其逆：

然后我打算证明 1) 一些长度为 n 的 0/1 列表等于2^^n，2) 函数是双射，3) 所以原始集合的基数2^^n也是。

这里有一些辅助定义和引理，看起来很有用：

这是最后一个引理：

这种方法看起来有效吗？有没有这样的证明的例子？你能提出一个关于如何证明引理的想法吗？我被卡住了，因为归纳set_to_bitmap.induct似乎在这里不适用。

我正在尝试在 Coq 中嵌入 HOL4 证明的可能性。

在 HOL 中，可以给出如下定义

是否有可能以类似的方式在 Coq 中定义这个函数？我的尝试在最后一行失败，原因是

编码：

补充：也许有一种定义 ALPHA 的方法，我们可以假设 t1=t2？（我的意思是，在 Coq 的标准平等意义上）。我不能添加假设（H：t1 = t2），但是我需要以某种方式进行匹配。如何进行相等的匹配？