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.