```
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?

```
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 ?

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
```

`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).

```
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