Substitution in Isabelle

问题:

In many paper proofs you see authors substitute variables in equations. For example, if there is an inequality "f(x-y) >= g(x-y)*z, the author simply writes let h=(x-y), therefore "f(h) >= g(h)*z" and continues with the proof.

To do the same in Isabelle, would I have to assume that h=(x-y), is there some other way of doing it? I looked at the "let" feature however that does something completely different.

Specifically, I have:

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)"

so I am letting h=y-x.

I can show this lemma if I assume that "∀h. ∀x∈S. ∀y∈S. h = y-x". Is this the correct approach?

回答1:

There are various possibilities to perform substitutions.

If you have some statement with meta-quantifier, you can just use where or of. To turn the quantifier ∀ in your formula into a meta-forall, you can for example use rule_format. Then, assms[rule_format, of x "h+x"] yields in your example the formula x ∈ S ⟹ x + h ∈ S ⟹ f (x + h) - f x >= (x + h - x) * g x.

Here, you immediately see two problems: first the difference between the - f x and the - g x, and the problem that it is not guaranteed that x + h ∈ S.

Alternative, you can also perform substitutions via unfolding, e.g., by using def h = "x - y" and then fold or unfold h_def.