Stream: Beginner Questions

Topic: THE


view this post on Zulip 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?

view this post on Zulip 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 ?

view this post on Zulip 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

view this post on Zulip Mathias Fleury (Jun 09 2021 at 04:52):

view this post on Zulip 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: Sep 25 2021 at 09:17 UTC