; File: single-event.lisp ; Author: Julien Schmaltz ; September 13th, 2001 ; University of Texas at Austin, Texas, USA ; visitor of University Joseph Fourier, Grenoble, France ; content: ; go-to-node without using mod (in-package "ACL2") ; Please adapt the ../../ to point to the right directory (include-book "../../../books/Arithmetic-4/bind-free/top") (set-non-linearp t) (include-book "../../../books/Arithmetic-4/floor-mod/floor-mod") ; First we redefine mod in term of equalities and inequalities (;defun mod-without-mod (x n) ; (if (and (rationalp x) ; (integerp n) ; (< 0 n)) ; (if (or (equal x 0) ; (integerp (/ x n))) ; 0 ; (if (< 0 x) ; (let ((k (floor x n))) ; (- x (* k n))) ; (let ((k (floor (- x) n))) ; (+ x (* (+ 1 k) n))))) ; 0)) ; the next definition seems to generate less cases in the proof of termination ; of go-to-node (defun mod-without-mod (x n) (if (and (rationalp x) (integerp n) (< 0 n)) (let ((k (floor (abs x) n))) (if (or (equal x 0) (integerp (/ x n))) 0 (if (< 0 x) (- x (* k n)) (+ x (* (+ 1 k) n))))) 0)) ;(defthm rationalp-mod-without-mod ; (implies (and (integerp n) ; (< 0 n) ; (rationalp x)) ; (rationalp (mod-without-mod x n)))) ;(defthm epsilon-0-mod-without-mod ; (e0-ordinalp (mod-without-mod x n))) (defthm mod-=-mod-without-mod (implies (and (integerp n) (rationalp x) (< 0 n)) (equal (mod x n) (mod-without-mod x n))) :hints (("GOAL" :cases ((equal x 0) (< 0 x) (< x 0)))) :rule-classes nil) ; I change every mod by mod-without-mod ; and it does not work at the first try!!!! ;------------------------------------------- ; ; Fixed size case: 8 nodes (defun clockwise (from) (mod-without-mod (+ 1 from) 8)) (defun counter-clockwise (from) (mod-without-mod (- from 1) 8)) (defun across (from) (mod-without-mod (+ 4 from) 8)) (defun go-to-node (dest from) (declare (xargs :measure (min (nfix (mod-without-mod (- dest from) 8)) (nfix (mod-without-mod (- from dest) 8))) :hints (("GOAL" :in-theory (disable prefer-positive-addends-< prefer-positive-addends-equal))))) (cond ((or (not (integerp dest)) (< dest 0) (< 7 dest) (not (integerp from)) (< from 0) (< 7 from)) nil) ((equal (- dest from) 0) nil) ((or (equal (mod-without-mod (- dest from) 8) 1) (equal (mod-without-mod (- dest from) 8) 2)) (cons from (go-to-node dest (clockwise from)))) ((or (equal (mod-without-mod (- dest from) 8) 6) (equal (mod-without-mod (- dest from) 8) 7)) (cons from (go-to-node dest (counter-clockwise from)))) (t (cons from (go-to-node dest (across from)))))) (defthm len-go-to-node-<=-2 (<= (len (go-to-node dest from)) 2))