*To*: isabelle-users at cl.cam.ac.uk*Subject*: Re: [isabelle] Modular arithmetic theory?*From*: Burkhart Wolff <bwolff at inf.ethz.ch>*Date*: Mon, 21 Nov 2005 11:53:36 +0100*In-reply-to*: <a46ee37bdce8de13521a82156a56ef3d@in.tum.de>*Organization*: ETH Zürich*References*: <1131631775.5258.95.camel@localhost.localdomain> <a46ee37bdce8de13521a82156a56ef3d@in.tum.de>

Am Freitag, den 18.11.2005, Amine Chaieb wrote: > > -An attempt to decide a challenge problem > > > > "(x div y) * y + (x mod y) = x" > > > > (div, mod, + * all 2's complement operations, > > such a property is required for the integers > > in the Java Language Specification) > > > > with an up-to-date wordlevel-BDD package > > was only feasible for a bit-length of 5 (!). > > why don't you use mod_div_equality (on nat) or zdiv_zmod_equality (on > int)? Seems that you not quite understood the problem, sorry. As I said, The div and mods, * and + are the 2's complement operations, so "(x::JavaInt) + y == Int_to_JavaInt (Rep_JavaInt x + Rep_JavaInt y)" where constdefs Int_to_JavaInt :: "int => JavaInt" "Int_to_JavaInt (x::int) == Abs_JavaInt(( ( x + (-MinInt_int)) mod (2 * (-MinInt_int))) + MinInt_int )" * and div and mod analogously. For div and mod the question is slightly obscured by the treatment of the signs. But: In the essence, around each operator, there is a "mod (2 * (-MinInt_int))". (you might ignore Abs_JavaInt and Rep_JavaInt as identities introduced by a type definition. Still, if you unfold the theorem above, you get a quite nasty expression with 4 "adjusting modulos", which are costly by theory. See http://kisogawa.inf.ethz.ch/WebBIB/publications/papers/2004/root.pdf for the full theory document). Therefore, we prove div_mod *on JavaInt* (i.e. on a standard 2's complement arithmetic for 32 Bit with a specific definition of the signs for div and mod), not on nat or int. The proof of the challenge problem used indeed zdiv_zmod_equality, but was still highly nontrivial. Nevertheless it is interesting *in itself* because it is required by the Java Language Specification. We started to get interested in the problem of deciding such problems automatically, since one of our referees claimed that this type of problems can be solved automatically, a claim, that we found completely unfounded. > Any way, presburger solves the problem above in 0.02 seconds. > Well, this theorem *is not* presburger arithmetic. I assume therefore, that your presburger arithmetic tactic makes a simplification step prior to further operations, and that zdiv_zmod_equality is simply in the rewriter set. Since zdiv_zmod_equality has been proven interactivly in the library, this is *not* an automatic proof in this theorem. Hope that helps, bu

**References**:**Re: [isabelle] Modular arithmetic theory?***From:*Burkhart Wolff

**Re: [isabelle] Modular arithmetic theory?***From:*Amine Chaieb

- Previous by Date: [isabelle] BCTCS 2006 - First Call for Participation
- Next by Date: Re: [isabelle] query about the isabelle tutorial slides
- Previous by Thread: Re: [isabelle] Modular arithmetic theory?
- Next by Thread: Re: [isabelle] Modular arithmetic theory?
- Cl-isabelle-users November 2005 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