0

我在伊莎贝尔有以下代码：

typedecl Person
consts age :: "Person ⇒ int" 

lemma "⟦(∀p::Person. age p > 20);p ∈ Person⟧⟹ age p > 20"
apply (auto)
done

自动证明方法工作正常并证明了引理！当我想将引理中前提的第一部分分解为定义 C1 时，如下所示：

definition C1::bool where "C1 ≡ (∀p::Person. age p > 20)"

auto方法无法在以下代码中证明：

lemma "⟦C1;p ∈ Person⟧⟹ age p > 20"
apply (auto)
done

为什么会这样？如果我在分解第一个假设的方式上做错了——我这样做是为了组织假设看起来整洁和结构化——不影响证明方法的最佳方法是什么（自动）功能。

谢谢

4

2 回答 2

1

该构造definition用作抽象实现细节的一种方式。它的用途之一是证明相关术语的某些属性，然后依赖属性而不是术语声明本身。因此，定义术语的简化规则不会自动添加到simpset. 这些规则仍然可以使用带有后缀的术语名称，_def并且可以显式使用：

lemma "⟦C1; p ∈ Person⟧ ⟹ age p > 20"
  apply (auto simp add: C1_def)
done
于 2014-11-07T06:04:19.350 回答
1

首先，为了实际添加一些价值，我将展示如何使用declare添加C1_def作为simp规则。然后我给你一些关于你的未经请求的指针lemma，然后我给你一些关于 Stackoverflow 礼仪的未经请求的指针（从我的角度来看）。

将定义声明为简单规则

正如 Alexander 指出的那样，adefinition通常不会自动添加simp。

您可以将其声明为如下simp规则：

declare C1_def [simp add]

通过自动证明方法auto, simp,fastforce等使用 simp 规则可能会导致错误的循环，或者以您不希望公式扩展的方式扩展公式，因此添加它之后，您可以将其删除为这样的simp规则：

declare C1_def [simp del]

评论你的引理

可能你的引理中的公式正是你想要的，但在我看来，你的符号是一个潜在的混淆来源。特别是，您将Person其用作类型名称和集合变量的名称。我发表这些评论时不要求澄清。

对我自己来说，我的问题是，“怎么p ∈ Person没有给出错误，因为Person有一个集合，其中Personintypedecl Person不是集合。

获取更多信息的一种方法是使用declare [[show_types, show_consts]].

为了回答我的问题，我执行了以下操作（为浏览器可移植性转换符号），并展示了我在输出面板中看到的一些内容：

declare [[show_types, show_consts]]
lemma "[|(!p::Person. age p > 20); p ∈ Person|] ==> (age p > 20)"
oops
(*OUTPUT:
  variables:
    Person :: Person set
    p :: Person *)

它告诉我这Person是一个自由变量。至于p，它是 中的一个绑定变量(!p::Person. age p > 20)，但在引理的其余部分是自由的，所以你的假设包括每个p类型Person都在每个类型集合中的公式Person set。

这可能是你想要的，但在这种情况下，它没有任何区别，因为你的引理基本上是形式A and B implies A。

您需要接受已回答的 SO 问题的答案

在我在大约 2 小时后消失之前，为了这个isabelle标签，我再次履行了作为 SO 礼仪警察的我心爱的职责。

你问了三个问题。特别是，有这样一个：

这是一个直截了当的问题，并且给出了直截了当的答案。您需要接受它作为答案。除此以外，

  • 当人们点击“伊莎贝尔”标签的“未回答”标签时，它可能会显示为未回答，当它未被回答时，
  • 对于给出的答案，您没有在应有的范围内表现出适当的赞赏。

对于我链接到的问题，您从 Isbelle/HOL 的一位专家那里得到了答案（与我不同）。一个人输入这样的答案需要花费大量时间。它不是特别长，但也不是单行的。

于 2014-11-07T14:59:23.693 回答