zibo yang (Jun 08 2021 at 20:51): 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
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: Apr 25 2024 at 08:20 UTC