Considering the theorem “P (t) ⟶ (∃x. P (x))” with object logical implication, why is the evidentiary goal “P (t) ⟹ (∃x. P (x))” given with the logical consequences?

Question

I am just starting with Isabelle / HOL and trying to prove a simple HOL instruction "P (t) ⟶ (∃x. P (x))" with natural deduction rules. I started with a theory file containing only a theorem:

theory simple imports Main begin lemma T: shows "P(t) ⟶ (∃x . P(x))" proof (* x *) qed end 

In the position marked x in the comment, the current target is already “P (t) ⟹ (∃x. P (x))”, i.e. logical implication is already simplified to meta-logical implication.

Through a trial version and an error, I came to the following proof:

 proof assume "P(t)" then have "∃ x . P(x)" by (rule exI) then have "P(t) ⟶ (∃x . P(x))" by (rule impI) then show "P(t) ⟹ (∃x . P(x))" by (rule impE) qed 

which looks kind of weird: I introduced the implication, just to eliminate it in the next step.

Now my questions are:

• Where does the rewriting of my goal come from and where can I find more about it?
• How to simplify the proof (without going around ND with a car)?

Answer 1

Where does the rewriting of my goal come from and where can I find more about it?

When you use proof like this, it takes one simple step to your goal. In your case, rule impI . If you do not want this, use proof - .

But you probably want to use the rule impI here. Note that this changes your purpose, and you can simply write:

 proof assume "P(t)" then show "∃ x . P(x)" by (rule exI) qed 

What is the answer to your second question.