Re: [isabelle] list_all vs set membership



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


On Wed, Oct 14, 2020 at 11:06 PM Jakub Kądziołka <kuba at kadziolka.net> wrote:
>
> 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.