How can I instantiate a variable in an existential quantifier in apply style

From Isabelle Community Wiki
Jump to: navigation, search

Sometimes, it is necessary to instantiate an existentially quantified variable in by hand.

Using rule_tac, it is possible to specify the desired instantiation by hand.

 lemma "∃ x. x = 3"
   apply(rule_tac x="3" in exI)
   apply simp


Using apply style is considered deprecated and should be avoided. Using Isar, the obtain keyword is available.

 lemma "∃ x. x = 3"
 proof -
   obtain y :: nat where "y = 3" by simp
   hence "∃ x. x = 3" using exI[where x="y"] by simp
   thus ?thesis .

The using exI[where x="y"] can be omitted.