Re: [isabelle] pred ... (map ... x) = pred ... x



Hi Lars,

> On 22 Mar 2016, at 15:38, Lars Hupel <hupel at in.tum.de> wrote:
> 
> Dear BNF developers,
> 
> may I suggest theorems of the following form to be generated by the
> datatype package?
> 
> theorem list_all_map:
>  fixes P :: "'a â bool"
>    and f :: "'b â 'a"
>    and xs :: "'b list"
>  shows "list_all P (map f xs) = list_all (Îx. P (f x)) xsâ

in a recent repository version (e.g. c4fad0569a24) you get list.pred_map:

theorem
  fixes Q :: "'a â bool" 
    and f :: "'b â 'a" 
    and x :: "'b list" 
  shows "list_all Q (map f x) = list_all (Q o f) xâ

Additionally unfolding o_def will give you what you want.

Dmitriy



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