Re: [isabelle] Cancellation lemmas for setprod and setsum



(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?


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.