*To*: Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>*Subject*: Re: [isabelle] linarith for enat*From*: Larry Paulson <lp15 at cam.ac.uk>*Date*: Mon, 9 Mar 2015 14:56:19 +0000*Cc*: Tobias Nipkow <nipkow at in.tum.de>, cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <54FD9521.4010006@inf.ethz.ch>*References*: <54F9BA93.7000106@inf.ethz.ch> <54FA04D1.2090401@in.tum.de> <A6A81BBD-8FF5-4E27-BB6F-637D6A0013C1@cam.ac.uk> <54FA08AC.7050604@in.tum.de> <54FD9521.4010006@inf.ethz.ch>

Personally I would prefer an approach that used the hyper-naturals instead of type enat. They have better algebraic properties, though you donât get a unique infinite number. Larry Paulson > On 9 Mar 2015, at 12:42, Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch> wrote: > > Hi Larry and Tobias, > > The idea with non-standard integers sound interesting, so I investigated a bit further. Linear arithmetic works for all types in linordered_dom thanks to the generic setup in Int.thy. Since the hyperreals are an instance thereof, linarith works for them. Unfortunately, the hypernaturals are not, so linarith does not work for them. However, I think that one could make it work. I tried to adapt the setup for ordinary naturals to hypernaturals. It did not work out of the box because hypnat is not a type constructor, but a synonym for "nat star" and the Lin_Arith.add_discrete_type only accepts type constructors. Therefore, I copied the hypnat type to a type constructor hypernat with typedef and did the adaptation there. I now have a setup that works for my tiny examples on hypernat such as "3 < x ==> 2 < (x :: hypernat)". But as I am no expert for linarith, I don't know whether it is complete. > > The next question is how this could be used to implement a solver or simproc on enat. I defined a function hnat_of_neat :: enat => hypernat that respects orders and commutes with numerals. Thus, one can transform the goal "3 < x ==> 2 < (x :: enat)" to "3 < hnat_of_enat x â 2 < hnat_of_enat x". Unfortunately, linarith fails to prove this goal, although it succeeds on the more general "3 < y ==> 2 < y", and I do not know why. > > - Do you think that this is a viable way to go? > > - Do I really need a copy hypernat of nat star just for the sake of having a type constructor? > > - Does linarith provide some support for going from enat to hypernat? I noticed that there is the function Lin_Arith.add_inj_const, but I do not know what this is good for. > > Best, > Andreas > > > On 06/03/15 21:06, Tobias Nipkow wrote: >> I strongly suspect linear arithmetic was never set up for any nonstandard type. >> >> Tobias >> >> On 06/03/2015 20:58, Larry Paulson wrote: >>> Perhaps the nonstandard integers are the solution here. Nonstandard theories satisfy all >>> the first-order properties of the corresponding standard theories. Iâm not sure what >>> state they are in, however. Was linear arithmetic ever set up for them? >>> >>> >>> Larry >>> >>>> On 6 Mar 2015, at 19:49, Tobias Nipkow <nipkow at in.tum.de> wrote: >>>> >>>> Dear Andreas, >>>> >>>> Unfortunately the linear arithmetic decision procedure does not work for extended >>>> numbers, we had investigated that as well. The decision procedure works for all types >>>> in a class that requires certain cancellation laws, probably x+y <= x+z ==> y <= z. >>>> This fails in the presence of infinities. >>>> >>>> This is a sore problem and the only way around it seems to be to eliminate the >>>> infinities first, i.e. reduce it to the basic type. But that has to be done by plain >>>> old deduction as it would be very tricky to integrate such a step into the existing >>>> decision procedure. >>>> >>>> Tobias >>>> >>>> On 06/03/2015 15:32, Andreas Lochbihler wrote: >>>>> Dear experts for linear arithmetic in Isabelle, >>>>> >>>>> I wondered why the simplifier can prove statements such as the following for >>>>> nat, int, rat, and real, but fails for enat. >>>>> >>>>> lemma "3 < x ==> 2 < x" >>>>> >>>>> I found that the linarith solver does it for nat, int, rat, and real. >>>>> Unfortunately, there seems to be no setup for enat (or ereal). I therefore >>>>> briefly tried to configure linarith for enat by mimicking what has been done for >>>>> nat. Since I do not know the workings of the linarith prover and could not find >>>>> any documentation on it, my attempt failed. I only got warnings such as "Linear >>>>> arithmetic should have refuted the assumptions. Please inform Tobias Nipkow." or >>>>> errors like "Linear arithmetic: failed to add thms". >>>>> >>>>> Is it in principle possible to configure linarith for enat? Is there any >>>>> documentation what rewrite rules, cancellation simprocs and the like it needs? >>>>> >>>>> Cheers, >>>>> Andreas >>>>> >>>> >>> >>

**Follow-Ups**:**Re: [isabelle] linarith for enat***From:*Andreas Lochbihler

**References**:**[isabelle] linarith for enat***From:*Andreas Lochbihler

**Re: [isabelle] linarith for enat***From:*Tobias Nipkow

**Re: [isabelle] linarith for enat***From:*Larry Paulson

**Re: [isabelle] linarith for enat***From:*Tobias Nipkow

**Re: [isabelle] linarith for enat***From:*Andreas Lochbihler

- Previous by Date: Re: [isabelle] linarith for enat
- Next by Date: Re: [isabelle] [isabelle-dev] What is this 3 levels of lambda calculi?
- Previous by Thread: Re: [isabelle] linarith for enat
- Next by Thread: Re: [isabelle] linarith for enat
- Cl-isabelle-users March 2015 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