Re: [isabelle] list_all vs set membership
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 ..
On Wed, Oct 14, 2020 at 11:06 PM Jakub Kądziołka <kuba at kadziolka.net> wrote:
> 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
This archive was generated by a fusion of
Pipermail (Mailman edition) and