Re: [isabelle] Cancellation lemmas for setprod and setsum



Am 13/08/2012 11:44, schrieb Lars Noschinski:
> 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.

I agree that this looks like the right approach. Your suggested lemma in
(generalized form) is a direct consequence of setprod_Un_disjoint:

[| finite A; finite B; A Int B = {} |]
==> setprod f (A Un B) = setprod f A * setprod f B

because A-B and B are disjoint.

Tobias





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