# [isabelle] Trying to simplify with setsum

Hi,

`I am trying to simplify a subgoal that contains an occurrence of
``setsum, using the theorem setsum_Un. However, Isabelle refuses to
``match the LHS of setsum_Un with the appropriate subterm. Here's a
``nonsensical lemma to show what I mean:
`
lemma

` "setsum (f::nat => nat) (ran ((a::nat ~=> nat) |` A) \<union> ran
``(a |` B)) = Z"
`
None of the following tactics work:
apply (subst setsum_Un)
apply (auto simp only: setsum_Un)
apply (erule_tac setsum_Un[THEN ssubst])

`I think I'm either missing something obvious, or else that the type
``'nat' has not been made an instance of the appropriate axclasses.
`
Thanks,
-john

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