*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Infinity - infinity = infinity*From*: Johannes Hölzl <hoelzl at in.tum.de>*Date*: Fri, 02 Dec 2016 17:06:59 +0100*In-reply-to*: <1480694447.29055.7.camel@in.tum.de>*Organization*: TU München*References*: <6592A55E-9169-4BBE-8D8E-5A2F8E7718C4@inria.fr> <1480694447.29055.7.camel@in.tum.de>

Am Freitag, den 02.12.2016, 17:00 +0100 schrieb Johannes HÃlzl: > Dear Jasmin, > > Are you sure your definition works? > > I don't think cancel_comm_monoid_add will ever hold for enat or > ennreal > for a reasonable definition of minus. "a + b - a = b" is independent > of > Âthe definition of minus: if a is â then we always get "â - a = b" With `independent` I mean that it does not work no matter how we define "_ - _": if a = â then we always get "â - â = b". So we will always find a "b" for which the equation fails. The extended numbers are quite unintuitive. If I wouldn't have Isabelle I would have proved a lot of very nice but unfortunately wrong theorems :-) - Johannes > I would love to have better support for minus on enat and ennreal. > Andreas added a couple of years ago support for cancellation of > additive and multiplicative terms. Maybe we can also add something > like > Âthis for minus? > > When I added ennreal I also thought about adding additional type > classes for enat and ennreal with a better support for non- > cancellable > monoids. I think we can factor out some theorems from existing type > classes, like add_diff_assoc2. Or the second rule of > cancel_comm_monoid_add. > > Â- Johannes > > > Am Freitag, den 02.12.2016, 16:01 +0100 schrieb Jasmin Blanchette: > > 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 > >

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

**Re: [isabelle] Infinity - infinity = infinity***From:*Johannes Hölzl

- Previous by Date: Re: [isabelle] Infinity - infinity = infinity
- Next by Date: Re: [isabelle] Infinity - infinity = infinity
- 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