*To*: Amine Chaieb <chaieb at informatik.tu-muenchen.de>*Subject*: Re: [isabelle] arith tactic*From*: John Matthews <matthews at galois.com>*Date*: Tue, 21 Feb 2006 16:03:32 -0800*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <Pine.GSO.4.60.0602171053420.18065@sunbroy2.informatik.tu-muenchen.de>*References*: <C5C18756-F875-432F-8A9B-E38D405A7C7D@galois.com> <43F2D30A.4040201@cse.unsw.edu.au> <05C22D76-4D87-431D-8C96-5B34F6F617D5@galois.com> <Pine.GSO.4.60.0602171053420.18065@sunbroy2.informatik.tu-muenchen.de>

Hi Amine, thanks for looking into this.

"(x :: mword) < y - 1 ==> x + 1 > x"

[| i < (nb - 1) mod 256; 0 <= nb; nb < 256; 0 <= i; i < 256 |] ==> i < (i + 1) mod 256

lemma incr_inbounds_easy: "(x :: mword) < y ==> x + 1 > x" by (auto simp add: mword_ops_defs split: mword_splits) I then wrote a seemingly equivalent subgoal: lemma incr_inbounds_easy2: "(x :: mword) <= y - 1 ==> x + 1 > x" apply (auto simp add: mword_ops_defs split: mword_splits)

1. !!nb. [|0 <= nb; nb < 256|] ==> (nb - 1) mod 256 < ((nb - 1) mod 256 + 1) mod 256 2. !!nb i. [|0 <= nb; nb < 256; 0 <= i; i < 256; i < (nb - 1) mod 256|] ==> i < (i + 1) mod 256 I then tried my case-splitting heuristic on the first subgoal, apply (case_tac "nb - 1 >= 0", auto) which Isabelle simplified to False!

Cheers, -john Amine Chaieb wrote:

John,The reasoning about mod in arith about mod and div is poor andenhancing it is on the TODO list.I recently wrote a more effitient implementation of the same QEalgorithm, which is able to solve your problem whithin 3 minutes,running in ML (without proofs) which is just a pitty.Presburger arithmetic is just too general to deal with mod and divin a practically acceptable manner. The decision problem inPresburger arithmetic is doubly exponential in space with respectto the largest constant occuring in the formula (255).The bigger issue is that we'll be encountering many, many subgoalslike this in our projects here, most of which involve reasoningabout machine arithmetic. So we're relying on arith to dischargethem automatically and efficiently.Could you give me a "description" of this formula class? Amine.

**References**:**[isabelle] arith tactic***From:*John Matthews

**Re: [isabelle] arith tactic***From:*John Matthews

**Re: [isabelle] arith tactic***From:*Amine Chaieb

- Previous by Date: [isabelle] thms_containing
- Next by Date: Re: [isabelle] thms_containing
- Previous by Thread: Re: [isabelle] arith tactic
- Next by Thread: [isabelle] Installation Isabelle : help needed
- Cl-isabelle-users February 2006 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