CODEWITHSUNDEEP
isabellequantifiers
user2757762
user2757762

Reputation:

Lemma/rule to allow substitution in universally quantified variable (Isabelle)

I have a goal which looks something like "\<forall>x. \<exists>y.\<forall>(z::real). P x y z". Is there a rule which immediately allows me to conclude "\<forall>x. \<exists>y.\<forall>(z::real). P x y (z-2)"? If there isn't, I'd appreciate general advice on how to prove this type of goal.

I know I can prove it by using lots of allI,exI, allE,exE, but it seems like there must be a quick and simple way.

Upvotes: 2

Views: 102

Answers (1)

larsrh
larsrh

Reputation: 2659

The following works in 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

You can use the try0 command to give you a list of proof methods that are able to solve the goal.

Upvotes: 1

Related Questions