条件重写规则与未知条件

Question

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

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

的最小例子如下所示：

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 

我发现在参考手册中的下段，所以我想我可以解决我的问题与自定义解算器。 但是，我从来没有真正触及伊莎贝尔的内部ML部分，也不知道从哪里开始。

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

Answer 1

Isabelle简化器本身从不会在条件重写规则的假设中实例化未知数。然而，求解器可以做到这一点，最可靠的是assumption。因此，如果complex_fact a b c字面上出现在目标的假设中（而不是被添加到simpset中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和c是免费不是一个好重写规则，因为在左侧头部符号不是一个常数，而是自由变量a。因此，简化器将不会使用方程a = b + c来替换a和b + c，而是用方程a = b + c的文字出现替换为True。您可以在简化器的踪迹中看到这个预处理（使用using [[simp_trace]]在本地启用它）。这就是为什么example_1工作，其他人不工作的原因。如果你可以改变你的左手边，使得头部符号有一个常数，那么在不写一个自定义求解器的情况下，应该有一些体面的自动化证明。

此外，您可以使用useComplexFact作为销毁规则，进行一些（有限）形式的转发推理。也就是，

using assms 
apply(auto dest!: useComplexFact) 

也可以在某些情况下工作。然而，这与在可伸缩性方面展开定义非常接近。

Answer 2

您可以在定义中指定，它应该在前面加上[simp]:这样的自动输送到简化器：

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

现在所有的例子引理应该是可以解决的直接using cf by simp。