伊莎贝尔换人

Question

在许多论文证明中，您会看到作者在方程式中替换变量。例如，如果存在不等式“f(x-y) >= g(x-y)*z”，作者简单写为 let h=(x-y)，因此“f(h) >= g(h)*z”并继续有证据。

要在 Isabelle 中做同样的事情，我是否必须假设 h=(x-y)，还有其他方法吗？我查看了“让”功能，但它的作用完全不同。

具体来说，我有：

lemma
fixes f g :: "real⇒real"
assumes "∀x∈S. ∀y∈S. f y - f x ≥ (y-x)*(g x)"
shows "∀x∈S. ∀h. f (x+h) - g x ≥ h*(g x)"

所以我让 h=y-x。

如果我假设“∀h.∀x∈S.∀y∈S.h = y-x”，我可以证明这个引理。这是正确的方法吗？

Answer 1

执行替换有多种可能性。

如果您有一些带有元量词的语句，您可以使用where 或of。要将公式中的量词 ∀ 转换为 meta-forall，例如可以使用 rule_format。然后，assms[rule_format, of x "h+x"] 在您的示例中产生公式x ∈ S ⟹ x + h ∈ S ⟹ f (x + h) - f x >= (x + h - x) * g x。

这里，你马上看到两个问题：首先- f x和- g x的区别，以及不能保证x + h ∈ S的问题。

或者，您也可以通过展开来执行替换，例如，使用def h = "x - y"，然后折叠或展开h_def。