*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Cancellation lemmas for setprod and setsum*From*: Manuel Eberl <eberlm at in.tum.de>*Date*: Mon, 13 Aug 2012 14:37:17 +0200*In-reply-to*: <5028ED65.30103@in.tum.de>*References*: <5028273E.9090102@in.tum.de> <5028CC66.9000101@in.tum.de> <5028DC3A.4070204@in.tum.de> <5028ED65.30103@in.tum.de>*User-agent*: Mozilla/5.0 (X11; Linux i686; rv:14.0) Gecko/20120714 Thunderbird/14.0

It can indeed be proven for comm_monoid_mult in a rather straightforward fashion: lemma setprod_diff: "⟦B ⊆ A; finite A⟧ ⟹ setprod f A = setprod f (A - B) * setprod f B" by (subgoal_tac "A - B ∪ B = A", subst setprod_Un_disjoint[symmetric], auto intro: finite_subset) And the corresponding cancellation lemmas for products over nat, int and real. I was unable to prove a general version of this with arbitrary types because the correctness lemmas for the real type coercion seem to be only available for specific types such as nat and int. (note the implicit coercion to real) lemma setprod_cancel_nat: fixes f::"'a ⇒ nat" assumes "B ⊆ A" and "finite A" and "∀x∈B. f x ≠ 0" shows "setprod f A / setprod f B = setprod f (A - B)" (is "?A / ?B = ?C") proof- from setprod_diff[OF assms(1,2)] have "?A = ?C * ?B" by auto moreover have "?B ≠ 0" using assms by (simp add: finite_subset) ultimately show ?thesis by simp qed (and similarly for int and real) To be more precise, if I tried to prove this for arbitrary types with some sort constraint, i.e. 'b::comm_monoid_mult, I always got stuck at some subgoal like "real (a * b) = real a * real b" which seemed to be unprovable. Do I really have to write three separate lemmas for nat, int and real or is there a way to do this once for arbitrary types? On 13/08/12 14:04, Tobias Nipkow wrote: > 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 >>>

**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

**Re: [isabelle] Cancellation lemmas for setprod and setsum***From:*Tobias Nipkow

- Previous by Date: Re: [isabelle] Cancellation lemmas for setprod and setsum
- Next by Date: Re: [isabelle] isabelle/jedit
- Previous by Thread: Re: [isabelle] Cancellation lemmas for setprod and setsum
- Next by Thread: [isabelle] CFP: Systems Software Verification (SSV'12)
- 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