来自lambda函数应用程序的Isabelle中令人讨厌的替换行为

Question

我经常遇到这个问题：所以我想知道是否有一个方便的解决方法。

Isabelle认为"(λg. a g) k"和"a k"是相同的。至少

lemma "(λg. a g) k = a k" 

可以解决by rule refl。很公平。但是，在这个（组合好的）示例中，Isabelle似乎将"(λg. a g) k"视为"a k"，这一事实妨碍了看起来完全有效的替代。

lemma blah:"(λg. a g) = (λg. sin g)"
  sorry

lemma "(λk. a k < ((b k)::'a :: {banach,real_normed_algebra_1, ord})) = (λk. (λg. a g) k < (λg. b g) k)"
  apply (subst blah)

没有理由使用正弦。我只需要一个方便的常量，并且添加了所有种类以使其进行类型检查。

Answer 1

现在我可以在Isabelle中尝试：将eta_contract设置为false可以避免收缩

lemma blah:"(λg. a g) = (λg. sin g)"
  supply [[eta_contract= false]]
  sorry

产量

1. (λg. a g) = (λg. sin g)

我不认为默认情况下有充分的理由激活它，但是如果您确实想要，可以使用以下方法来激活它：

declare [[eta_contract= false]]