*To*: Amine Chaieb <chaieb at in.tum.de>*Subject*: Re: [isabelle] arith on large modulus*From*: John Matthews <matthews at galois.com>*Date*: Sun, 20 Jul 2008 19:17:19 -0700*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <4881A727.1050200@in.tum.de>*References*: <8483E474-CF2A-490D-A5A9-26464E5A4845@galois.com> <48818736.5040509@in.tum.de> <4881A727.1050200@in.tum.de>

Ok, thanks for looking into this, Amine. -john On Jul 19, 2008, at 1:34 AM, Amine Chaieb wrote:

Hi John,There is a problem converting this goal into a goal over int. Thenew goal after conversion still contains nat and int, which whichthe core presburger tactic can not cope. We need a more cleverconversion, which takes numerals into account, which occur in astatement containing both nat and int with explicit conversions (natand int).This could be more involved than the actual approach, an I think wecan not come around a specialized procedure -- i.e. a conversion ora set of simprocs + rules.Amine.PS: We could think about adding some intro rules to presburger ifsuch statements occur often. Candidates are mod_pos_pos_trivial andmod_less and others, to prove that some modulo operations arebasically the same as the usual operations assuming that the inputis within the size of the modulus.Tobias Nipkow wrote:It appears there is a bug. Which is not so easy do diagnose :-( Tobias John Matthews schrieb:Hi, I would like to automatically prove the following lemma: lemma "[|\<not> 100 < nat (x); 0 \<le> x|] ==> nat x + 11 = nat ((x + 11) mod 4294967296)"I thought this fell within the fragment that arith can handle, butit can't seem to prove it. I know how to prove this manually, butis there something else I can use to prove it in a single command?Thanks, -john

**References**:**[isabelle] arith on large modulus***From:*John Matthews

**Re: [isabelle] arith on large modulus***From:*Tobias Nipkow

**Re: [isabelle] arith on large modulus***From:*Amine Chaieb

- Previous by Date: [isabelle] Partially terminating functions
- Next by Date: Re: [isabelle] Partially terminating functions
- Previous by Thread: Re: [isabelle] arith on large modulus
- Next by Thread: [isabelle] LPAR'08 workshops
- Cl-isabelle-users July 2008 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