; 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))