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