[isabelle] list_all vs set membership



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




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.