*To*: Lawrence Paulson <lp15 at cam.ac.uk>, Tobias Nipkow <nipkow at in.tum.de>*Subject*: Re: [isabelle] Infinity - infinity = infinity*From*: Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>*Date*: Fri, 2 Dec 2016 17:26:23 +0100*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <0D695991-90BA-46EB-A25F-4FFF3CCFF1AA@cam.ac.uk>*References*: <6592A55E-9169-4BBE-8D8E-5A2F8E7718C4@inria.fr> <2956700a-dc8e-f201-a811-c5c3e3c3a87a@in.tum.de> <0D695991-90BA-46EB-A25F-4FFF3CCFF1AA@cam.ac.uk>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:45.0) Gecko/20100101 Thunderbird/45.4.0

llength (lappend xs ys) = llength xs + llength ys

Andreas On 02/12/16 17:09, Lawrence Paulson wrote:

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. --lcpOn 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. TobiasOn 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

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