伊莎贝尔换人
Substitution in Isabelle
在许多论文证明中，您会看到作者在方程式中替换了变量。例如，如果存在不等式 "f(x-y) >= g(x-y)*z, the author simply writes let h=(x-y), therefore "f(h) >= g(h)*z" 并继续证明。
要在 Isabelle 中做同样的事情，我是否必须假设 h=(x-y)，还有其他方法吗？我查看了 "let" 功能，但它的作用完全不同。
具体来说，我有：
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”，我可以证明这个引理。这是正确的做法吗？
执行替换有多种可能性。
如果你有一些带有元量词的语句，你可以只使用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.
在许多论文证明中，您会看到作者在方程式中替换了变量。例如，如果存在不等式 "f(x-y) >= g(x-y)*z, the author simply writes let h=(x-y), therefore "f(h) >= g(h)*z" 并继续证明。
要在 Isabelle 中做同样的事情，我是否必须假设 h=(x-y)，还有其他方法吗？我查看了 "let" 功能，但它的作用完全不同。
具体来说，我有：
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”，我可以证明这个引理。这是正确的做法吗？
执行替换有多种可能性。
如果你有一些带有元量词的语句，你可以只使用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.