*To*: Brian Huffman <brianh at cse.ogi.edu>*Subject*: Re: [isabelle] Trying to simplify with setsum*From*: John Matthews <matthews at galois.com>*Date*: Wed, 30 Nov 2005 07:37:22 -0800*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <200511291727.09394.brianh@cse.ogi.edu>*References*: <8A62FB54-3A2B-4B2D-90C3-A1DE96F351B6@galois.com> <200511291727.09394.brianh@cse.ogi.edu>

Thanks Brian, that did the trick. -john On Nov 29, 2005, at 5:27 PM, Brian Huffman wrote:

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

**References**:**[isabelle] Trying to simplify with setsum***From:*John Matthews

**Re: [isabelle] Trying to simplify with setsum***From:*Brian Huffman

- Previous by Date: Re: [isabelle] real number calculation
- Next by Date: [isabelle] recdef woes
- Previous by Thread: Re: [isabelle] Trying to simplify with setsum
- Next by Thread: [isabelle] recdef woes
- Cl-isabelle-users November 2005 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list