*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Infinity - infinity = infinity*From*: Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de>*Date*: Wed, 7 Dec 2016 17:52:30 +0100*In-reply-to*: <2956700a-dc8e-f201-a811-c5c3e3c3a87a@in.tum.de>*Organization*: TU Munich*References*: <6592A55E-9169-4BBE-8D8E-5A2F8E7718C4@inria.fr> <2956700a-dc8e-f201-a811-c5c3e3c3a87a@in.tum.de>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:45.0) Gecko/20100101 Thunderbird/45.5.1

Just to add another remark on this thread: AFAIU, Ââ - âÂ is similar to Â1 / 0Â: there is no definition for it that satisfied fundamental desired algebraic properties. Florian Am 02.12.2016 um 16:57 schrieb Tobias Nipkow: > Jasmin, there is a reason why I would not do this: > > Aless Lasaruk and Thomas Sturm. > Effective Quantifier Elimination for Presburger Arithmetic with Infinity > > This paper shows that our current enat has quantifier elimination > (although we have not inplemented it, and it would be some work, but not > infeasible). In their system, "â - â = â". Unless we know that your > proposed modification still has quantifier elimination, I would be > reluctant to give up that strong property. > > Tobias > > On 02/12/2016 16:01, Jasmin Blanchette wrote: >> Dear all, >> >> As noted before on this mailing list, automation for "enat" >> ("Library/Extended_Nat.thy") is quite poor. Often, the only way to >> proceed is to perform case distinctions on all "enat" and use auto on >> the emerging subgoals. >> >> My impression is that many type classes are not available because of >> the definition of subtraction. Because "â - â = â" (where "â" is the >> infinity symbol), we lack one of the two properties required by >> "cancel_comm_monoid_add": >> >> 1. âa b. a + b - a = b >> 2. âa b c. a - b - c = a - (b + c) >> >> and we lack the third property required by "comm_semiring_1_cancel": >> >> 3. âa b c. a * (b - c) = a * b - a * c >> >> Counterexample for 1: a = â, b = 0. >> Counterexample for 3: a = â, b = c = 1. >> >> These omissions affect further layers in the type class hierarchy -- >> e.g. we cannot use "ordered_cancel_comm_monoid_diff", even though some >> of its theorems (e.g. "add_diff_assoc2") turn out to hold. >> >> My proposal is to change the definition of subtraction so that "â - â >> = 0" and to instantiate the missing type classes. I believe this would >> make "enat" much less painful to use, and mathematically I'm not so >> convinced that "â - â = â" is such a great idea anyway. Indeed, I have >> recently implemented ordinals below Î_0 in Isabelle and was able to >> have much better automation than with "enat", and there we have Ï - Ï >> = 0. >> >> "enat" occurs in about 70 ".thy" files in Isabelle and the AFP, so >> this change (including the type class instantiations) seems quite >> manageable. We (= Mathias and I) would wait until after the 2016-1 >> release to avoid any interference. >> >> Any opinions for or against? >> >> Jasmin >> >> > -- PGP available: http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

**Attachment:
signature.asc**

**References**:**[isabelle] Infinity - infinity = infinity***From:*Jasmin Blanchette

**Re: [isabelle] Infinity - infinity = infinity***From:*Tobias Nipkow

- Previous by Date: Re: [isabelle] Infinity - infinity = infinity
- Next by Date: [isabelle] PiP 2017: Principles in Practice - Call for Participation
- Previous by Thread: Re: [isabelle] Infinity - infinity = infinity
- Next by Thread: Re: [isabelle] Infinity - infinity = infinity
- Cl-isabelle-users December 2016 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