대체로 정량화 된 변수 (Isabelle)에서 대체를 허용하는 보조 정리/규칙

Question

목표는 "\<forall>x. \<exists>y.\<forall>(z::real). P x y z"입니다. 즉시 "\<forall>x. \<exists>y.\<forall>(z::real). P x y (z-2)"을 결론 지을 수있는 규칙이 있습니까? 그렇지 않은 경우이 유형의 목표를 증명하는 방법에 대한 일반적인 조언에 감사드립니다.

은 내가 allI, exI, allE, exE을 많이 사용하여 증명할 수 알지만, 빠르고 간단한 방법이있을 것처럼 보인다.

Answer 1

Isabelle2016-1-RC2의 다음 작품 :

lemma 
    assumes "∀x. ∃y.∀(z::real). P x y z" 
    shows "∀x. ∃y.∀(z::real). P x y (z-2)" 
using assms by force 

당신은 당신이 목표를 해결할 수있는 증거 방법의 목록을 제공하기 위해 try0 명령을 사용할 수 있습니다.