问题标签 [isar]

我正在尝试linordered_field_class.frac_le在 Isar 证明中使用该规则。这是代码片段（它可能取决于证明的前面部分，但这不太可能）。n是 nat 类型。

我认为我已正确应用该规则，但它抱怨“无法完成证明”。我认为这可能是类型错误，因此使用 过度杀伤:: real，但我无法修复它。有谁知道可能是什么问题，以及如何解决？或者只是证明这种陈述的另一种方法。

有谁知道显示规则

在现实中？

我使用“查询”面板找到了以下规则：

虽然我有点困惑是什么op意思。

我希望能够通过对 n（nat 类型）的归纳来证明一个陈述。它由一个前提条件组成，其前提条件仅在 n >= 2 时为真。前提条件为假的条件始终为真。所以我想证明 n=0、n=1 和 n=2 的情况都与主要归纳步骤分开。是否可以通过以下三个基本案例进行归纳证明：

就目前而言，这似乎不起作用。我可以"P (n+2) --> Q"通过归纳来证明，但这不会是一个强有力的陈述。我正在考虑将一个案例拆分为"n=0","n=1"和"n>=2", 并仅通过归纳证明最后一个案例。

我正在尝试解决Isabelle 中的 Programming and Proving 中的练习 4.7 。我遇到了一个案例，我证明了 False 并因此证明了所有内容，但我无法结案，因为我不知道如何提及我的证明义务。

最后一个命题show是从 Isabelle/jedit 中的证明状态复制而来的。但是，Isabelle 报告了错误（在最后show）：

现在被注释掉的证明目标导致了同样的错误。如果我将案例交换为0and Suc，则错误出现在最后一个show案例0中，但不再出现在Suc案例中。

有人可以解释为什么伊莎贝尔不会在这里接受这些看似正确的目标吗？我如何以 Isabelle 接受的方式陈述子目标？是否有指代当前子目标的一般方式？我认为考虑到我使用的构造，?case应该完成这项工作，但显然它没有。

我发现这个Stack Overflow question 提到了相同的错误，但是问题不同（定理存在一个等价性，应该通过隐式应用将其拆分为方向子目标rule）并且应用所提供的解决方案会导致不正确且无法证明就我而言，目标。

我想知道如何在以下情况下重新排序目标：

我想要一个不涉及更改引理语句的解决方案。我意识到这一点prefer并且defer可以用于应用风格的证明，但我希望有一种可以在proof (...)零件中使用的方法。

编辑：

正如 Andreas Lochbihler 所说，rule iffI[rotated]在上面的例子中写作是有效的。但是，在不改变引理陈述的情况下，是否可以在以下情况下交换目标顺序？

这个例子可能看起来做作，但我觉得可能存在不方便改变引理的陈述的情况，或者在之前没有应用诸如iffI.

假设我想证明∃ n m k . [n, m, k] = [2, 3, 5]Isabelle/Isar 中的引理。如果我按照第 45 页的 Isabelle/HOL 教程中的建议继续，我的证明如下所示：

当然，这太冗长了。我如何证明上述命题，以使证明简洁易读？

Isabelle 是否可以访问数据类型的各个元素？假设我有以下数据类型：

和（例如在引理中）

是否可以访问 A 的单个元素？或者，修复单个元素 ( fix a b c d :: int)，然后定义A为mat a b c d?

Isabelle 在证明陈述时是否支持自定义案例区分？假设我想证明所有自然数的陈述n，但证明是完全不同的，取决于n是偶数还是奇数。是否可以在证明中区分这种情况，例如

到目前为止，我将引理/定理分成两个单独的部分（假设n偶数/奇数），然后使用这些部分来证明所有自然数的陈述，但这似乎不是最佳解决方案。