0

在我的理论中，我有一些更大的定义，我使用引理从中推导出一些简单的属性。

我的问题是，简化器不使用派生属性的引理，我必须手动实例化它们。有没有办法让它更自动化？

一个最小的例子如下所示：

definition complexFact :: "int ⇒ int ⇒ int ⇒ bool" where
"complexFact x y z ≡ x = y + z"

lemma useComplexFact: "complexFact x y z ⟹ x = y + z"
by (simp add: complexFact_def)

lemma example_1:
assumes cf: "complexFact a b c"
shows "a = b + c"
apply (simp add: cf useComplexFact) (* easy, works *)
done

lemma example_2a:
assumes cf: "complexFact a b c"
shows "a - b = c"
apply (simp add: cf useComplexFact) (* does not work *)
oops

lemma example_2b:
assumes cf: "complexFact a b c"
shows "a - b = c"
apply (simp add: useComplexFact[OF cf]) (* works *)
done

lemma example_2c:
assumes cf: "complexFact a b c"
shows "a - b = c"
apply (subst useComplexFact) (* manually it also works*)
apply (subst cf)
apply simp+
done

我在参考手册中找到了以下段落，所以我想我可以使用自定义求解器解决我的问题。但是，我从来没有真正接触过 Isabelle 的内部 ML 部分，也不知道从哪里开始。

重写不会实例化未知数。例如，单独重写不能证明 a ∈ ?A 因为这需要实例化 ?A 。然而，求解器是一种任意策略，可以随意实例化未知数。这是 Simplifier 可以处理条件包含额外变量的条件重写规则的唯一方法。

4

1 回答 1

3

Isabelle 简化器本身从不实例化条件重写规则假设中的未知数。但是，求解器可以做到这一点，最可靠的是assumption. 因此，如果complex_fact a b c从字面上出现在目标的假设中（而不是添加到带有simp add:或的简化集中[simp]），假设求解器就会启动并实例化未知数。但是，它只会使用complex_fact假设中的第一个实例。所以如果有几个，它不会尝试所有的。总之，最好写

lemma
  assumes cf: "complexFact a b c"
  shows "a = b + c"
  using cf
  apply(simp add: useComplexFact)

您的示例的第二个问题是a = b + c使用a,b和cfree 不是一个好的重写规则，因为左侧的头符号不是常数，而是自由变量a。因此，简化器不会使用等式a = b + c来替换a，而是用 来替换等式的b + c文字出现。您可以在 simplifer 的跟踪中看到此预处理（使用 本地启用它）。这就是为什么有效而其他无效的原因。如果你可以改变你的左手边，使得有一个常量作为头部符号，那么在不编写自定义求解器的情况下，应该可以实现一些体面的证明自动化。a = b + cTrueusing [[simp_trace]]example_1

此外，您可以通过useComplexFact用作破坏规则来进行某些（有限）形式的前向推理。那是，

using assms
apply(auto dest!: useComplexFact)

在某些情况下也可以工作。但是，这非常接近于在可扩展性方面展开定义。

于 2016-08-02T17:40:23.900 回答