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