help on "THE: definite description operator"

[Massimo Zaniboni]

Hi,

I'm new of Isabelle, and I like it very much. I tried successfully some proofs, but now I'm stuck with this apparently simple proof:

lemma THE_exist:
fixes P :: "'a ⇒ bool"
assumes a1: "∃ a . a = (THE b . P b)"
shows "∃ a . P a"
sorry

My most promising partial attempt is this:

lemma THE_exist:
fixes P :: "'a ⇒ bool"
assumes a1: "∃ a . a = (THE b . P b)"
shows "∃ a . P a"
proof -
from a1 have "∃ a . a = (SOME b . P b)" by auto
from this obtain a where a: "a = (SOME b . P b)" by auto

(* TODO trying to use this lemma of the library:

lemma some_eq_ex: "P (SOME x. P x) ⟷ (∃x. P x)"
by (blast intro: someI)
*)

qed

Any hint will be very appreciated!
Massimo