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



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"

Cheers
Lars




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