*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Cancellation lemmas for setprod and setsum*From*: Tobias Nipkow <nipkow at in.tum.de>*Date*: Mon, 13 Aug 2012 14:04:53 +0200*In-reply-to*: <5028DC3A.4070204@in.tum.de>*References*: <5028273E.9090102@in.tum.de> <5028CC66.9000101@in.tum.de> <5028DC3A.4070204@in.tum.de>*User-agent*: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.6; rv:14.0) Gecko/20120713 Thunderbird/14.0

Am 13/08/2012 12:51, schrieb Manuel Eberl: > (Replied directly at first instead of to the list, sorry about that) > > No, I really meant /. I have coercions from nat to real in there. But > yes, the generalisation you proposed seems like a good idea, that should > work for any abelian semigroup with multiplication, I think. (as long as > the underlying lemmas for setprod are that general as well) > > I was just very surprised that something like this didn't exist already. > Who is responsible for maintaining these libraries, i.e. whom do I have > to contact if I have a lemma that I think should be included in the library? You can try to send it to one of the people who created the theory. Which would be me in this case. Tobias > > On 13/08/12 11:44, Lars Noschinski wrote: >> On 12.08.2012 23:59, Manuel Eberl wrote: >>> Hallo, >>> >>> I recently needed something like a "cancellation lemma" for setprod but >>> was unable to find anyting like it in the libraries. >>> >>> The lemma I needed and proved was the following: >>> lemma setprod_cancel: fixes A::"nat set" and B::"nat set" >>> assumes "B ⊆ A" and "finite A" and "0 ∉ B" shows "∏A / ∏B = ∏(A-B)" >> >> Did you mean "div" instead of "/" or do you an implicit conversion to >> real in there? >> >>> Is there a lemma like this somewhere? If yes, what is it called? If >> not, >>> it might be a good idea to add this (or a generalised version of this) >>> and a version for setsum to the libraries, since it seems like >> something >>> one needs quite often when dealing with products and sums. >> >> For sums, there is setsum_diff. For products, there is the question >> what the type class of the base type of A,B should be -- probably >> would need to be a field, to be useful (which then excludes the >> naturals). >> >> Maybe one could generically prove "∏A = ∏(A-B) * ∏B" and derive your >> variant from there for specific types. >> >> -- Lars >> >

**Follow-Ups**:**Re: [isabelle] Cancellation lemmas for setprod and setsum***From:*Manuel Eberl

**References**:**[isabelle] Cancellation lemmas for setprod and setsum***From:*Manuel Eberl

**Re: [isabelle] Cancellation lemmas for setprod and setsum***From:*Lars Noschinski

**Re: [isabelle] Cancellation lemmas for setprod and setsum***From:*Manuel Eberl

- Previous by Date: Re: [isabelle] Cancellation lemmas for setprod and setsum
- Next by Date: Re: [isabelle] Cancellation lemmas for setprod and setsum
- Previous by Thread: Re: [isabelle] Cancellation lemmas for setprod and setsum
- Next by Thread: Re: [isabelle] Cancellation lemmas for setprod and setsum
- Cl-isabelle-users August 2012 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