; File: fixed-size-case.lisp
; Author: Julien Schmaltz
; September 12th, 2001
; University of Texas at Austin, Texas, USA
; visitor of University Joseph Fourier, Grenoble, France

; content: 
; listp code for the fixed size algorithm presented in the talk

(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")


(defun clockwise (from)
  (mod (+ 1 from) 8))

(defun counter-clockwise (from)
  (mod (- from 1) 8))

(defun across (from)
  (mod (+ 4 from) 8))

(defthm <-7
  (implies (and (integerp x) (<= 0 x))
           (equal (< 7 x)
                  (and (not (equal x 0))
                       (not (equal x 1))
                       (not (equal x 2))
                       (not (equal x 3))
                       (not (equal x 4))
                       (not (equal x 5))
                       (not (equal x 6))
                       (not (equal x 7))))))

(defun go-to-node (dest from)
  (declare (xargs :measure (min (nfix (mod (- dest from) 8))
                                (nfix (mod (- from dest) 8)))))
  (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 (- dest from) 8) 1)
             (equal (mod (- dest from) 8) 2))
         (cons from (go-to-node dest (clockwise from))))
        ((or (equal (mod (- dest from) 8) 6)
             (equal (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))