## Stream: Beginner Questions

### Topic: THE

#### zibo yang (Jun 08 2021 at 20:51):

``````lemma test:
fixes A
assumes "∃i::nat. enat (THE a. a ∈ A ∧ a < 1) = enat i""A = {0,1}"
obtains b where "enat b = enat (THE a. a ∈ A ∧ a < 1) ∧ b ∈ A"
using enat.inject assms
``````

I didn't get the point why this simple lemma was not proved by sledgehammer or myself. Is there any assumption lost there?

#### zibo yang (Jun 08 2021 at 23:18):

``````lemma test2:
fixes A
assumes "enat i = enat (SOME a. a ∈ A ∧ a<1)" "A ={0,1,10}"
shows "i ∈ A"
using enat.inject assms
by blast

lemma  test3:
fixes A
assumes "i = (SOME a. a ∈ A ∧ a<1)" "A ={0,1,10}"
shows "i ∈ A"
using assms
by blast
``````

Another weird thing is that there is just a little change from test2 to test3, but blast can prove the test2 and fail on test3. Why does it fail? can anyone explain to me the definition or the difference bewteen SOME and THE ?

#### Mathias Fleury (Jun 09 2021 at 04:51):

Your are missing a type annotation that is implicit in test2:

``````lemma  test3:
fixes A and i :: nat
assumes "i = (SOME a. a ∈ A ∧ a<1)" "A ={0,1,10}"
shows "i ∈ A"
using assms
by blast
``````

#### Mathias Fleury (Jun 09 2021 at 04:52):

• `SOME x. P x` is _one_ undefined element that fulfills `P x` (if any exists).
• `THE x. P x` is _the_ unique element that fulfills `P x` (if any exists).

#### Mathias Fleury (Jun 09 2021 at 04:53):

``````thm theI someI
(*
?P ?a ⟹ (⋀x. ?P x ⟹ x = ?a) ⟹ ?P (THE x. ?P x)
?P ?x ⟹ ?P (Eps ?P)
*)
``````

Last updated: Aug 10 2022 at 20:22 UTC