Замена в Isabelle

Question

Во многих бумажных доказательствах вы видите, что авторы заменяют переменные в уравнениях. Например, если существует неравенство «f (xy)> = g (xy) * z, то автор просто пишет let h = (xy), поэтому« f (h)> = g (h) * z "и продолжается с доказательством.

Чтобы сделать то же самое в Изабель, я должен был предположить, что h = (xy), есть ли другой способ сделать это? Я посмотрел на функцию «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. ∀x∈S. ∀y∈S. ч = уи». Это правильный подход?

Answer 1

Существуют различные возможности для выполнения замены.

Если у вас есть заявление с мета-квантора, вы можете просто использовать where или of. Чтобы включить квантор ∀ в формуле в мета-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.