# Re: [isabelle] Trying to simplify with setsum

Here is the theorem setsum_Un, printed with sorts shown:
[| finite (?A::?'b::type set); finite (?B::?'b::type set) |]
==> setsum (?f::?'b::type => ?'a::ab_group_add) (?A Un ?B) =
setsum ?f ?A + setsum ?f ?B - setsum ?f (?A Int ?B)
The result type of "f" must be an additive abelian group, having additive
inverses, which "nat" does not. Since subtraction on type "nat" has some
unusual properties, I would not expect many polymorphic theorems about
subtraction to apply to naturals. I would guess that a version of setsum_Un
still holds for naturals, but it would need a separate proof.
- Brian
On Tuesday 29 November 2005 17:07, John Matthews wrote:
> 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.*