Re: [isabelle] Infinity - infinity = infinity



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




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.