Given a theorem "P(t) ⟶ (∃x . P(x))" with an object logic implication, why is the proof goal "P(t) ⟹ (∃x . P(x))" given with meta-logic implication?

Question

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

theory simple imports Main
begin

lemma T: shows "P(t) ⟶ (∃x . P(x))"
proof
  (* x *)
qed  

end

At the position marked x in the comment, the current goal is already "P(t) ⟹ (∃x . P(x))", i.e. the logical implication is already simplified to meta-logical implication.

Via trial and 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 somehow odd: I am introducing the implication, just to eliminate it in the next step.

My questions now are:

1. Where does the rewriting of my goal come from and where can I find more about it?
2. How would I simplify the proof (without circumventing ND by using auto)?

Answer 1

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

When you use proof like that, it applies one simple step towards your goal. In your case, it applies rule impI. If you do not want that, use proof -.

But you probably do want to use the implicit rule impI here. Note that it changes your goal, and you can just write:

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

Which answers your second question.