*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:33:39 +0100*In-reply-to*: <0D695991-90BA-46EB-A25F-4FFF3CCFF1AA@cam.ac.uk>*Organization*: TU München*References*: <6592A55E-9169-4BBE-8D8E-5A2F8E7718C4@inria.fr> <2956700a-dc8e-f201-a811-c5c3e3c3a87a@in.tum.de> <0D695991-90BA-46EB-A25F-4FFF3CCFF1AA@cam.ac.uk>

Am Freitag, den 02.12.2016, 16:09 +0000 schrieb Lawrence Paulson: > As a rule, people should use non-standard analysis rather than the > extended naturals or reals. Although the former are more complicated, > they preserve all the first order properties of their standard > counterparts. In particular, the non-standard naturals are still a > semiring.Â Hm, enat also forms a semiring: Â instantiation enat :: "{comm_semiring_1, semiring_no_zero_divisors}" > --lcp > > On 2 Dec 2016, at 15:57, Tobias Nipkow <nipkow at in.tum.de> wrote: > > > > 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 > > > > > > > >

**Follow-Ups**:**Re: [isabelle] Infinity - infinity = infinity***From:*Lawrence Paulson

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

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

**Re: [isabelle] Infinity - infinity = infinity***From:*Lawrence Paulson

- 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