How can I instantiate a variable in an existential quantifier in apply style
Sometimes, it is necessary to instantiate an existentially quantified variable in by hand.
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 done
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 . qed
using exI[where x="y"] can be omitted.