Re: [isabelle] Trying to simplify with setsum



It turns out there is a version of "setsum_Un" for naturals: try using 
"setsum_Un_nat" instead.

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