Re: [isabelle] Cancellation lemmas for setprod and setsum

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.


> 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

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.