[isabelle] Trying to simplify with setsum


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:

"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.


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