Say I want to prove the lemma ∃ n m k . [n, m, k] = [2, 3, 5] in Isabelle/Isar. If I go ahead as suggested in the Isabelle/HOL tutorial on page 45, my proof looks as follows:
lemma "∃ n m k . [n, m, k] = [2, 3, 5]"
proof
show "∃ m k . [2, m, k] = [2, 3, 5]"
proof
show "∃ k . [2, 3, k] = [2, 3, 5]"
proof
show "[2, 3, 5] = [2, 3, 5]" by simp
qed
qed
qed
Of course, this is way too verbose. How can I prove propositions like the above one such that the proofs are concise and readable?
Multiple existential quantifiers can be introduced in a single step by applying the single-quantifier introduction rule several times. For example, the proof method (rule exI)+ introduces all outermost existential quantifiers.
lemma "∃n m k. [n, m, k] = [2, 3, 5]"
proof(rule exI)+
show "[2, 3, 5] = [2, 3, 5]" by simp
qed
Alternatively, you can first state the instantiated property and then use an automatic proof method to do the instantiations. Usually blast works well here because it does not invoke the simplfier. In your example, you will have to add type annotations because numbers are overloaded.
lemma "∃n m k :: nat. [n, m, k] = [2, 3, 5]"
proof -
have "[2, 3, 5 :: nat] = [2, 3, 5]" by simp
then show ?thesis by blast
qed