[isabelle] list_all vs set membership
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
This archive was generated by a fusion of
Pipermail (Mailman edition) and