Re: [isabelle] list_all vs set membership



On Thu, Oct 15, 2020 at 12:06 AM 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
>

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




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