Email Gateway (Oct 14 2020 at 22:04): Email Gateway (Oct 14 2020 at 22:04):From: Jakub Kądziołka <kuba@kadziolka.net>
Hello,
many theorems in Main express a condition on all elements of a list with
"⋀x. x ∈ set xs ⟹ P x". However, one could also say that with
"list_all P xs". I am quite surprised that there is no lemma allowing to
freely convert between the two (or, at least, I couldn't find it).
I'd therefore like to suggest the following addition:
lemma list_all_iff_forall_set [iff]:
"list_all P xs ⟷ (∀x. x ∈ set xs ⟶ P x)"
by (induction xs) auto
Kind regards,
Jakub Kądziołka
Email Gateway (Oct 14 2020 at 22:32):From: Andrei Popescu <andrei.h.popescu@gmail.com>
Hi Jakub,
The definition of list_all already expresses something very similar:
lemma list_all_iff_forall_set [iff]:
"list_all P xs ⟷ (∀x. x ∈ set xs ⟶ P x)"
unfolding list_all_def Ball_def ..
Best wishes,
Andrei
Email Gateway (Oct 15 2020 at 07:59):From: Lawrence Paulson <lp15@cam.ac.uk>
I would avoid the [iff] attribute, since users may not want to have list_all rewritten away.
Larry
Email Gateway (Oct 15 2020 at 08:20):From: Lukas Bulwahn <lukas.bulwahn@gmail.com>
As far as I recall years ago, the list_all constant was introduced for
tools, code generation, etc., but it is really not intended for 'user'
theories. Just use the facts on "⋀x. x ∈ set xs ⟹ P x". Generally all
user tools are smart enough to conclude the same on '⋀x. x ∈ set xs ⟹
P x" compared to 'list_all P xs'.
I hope this helps.
Lukas
Last updated: Jul 15 2022 at 23:21 UTC