; File: single-event.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 proof as a single event

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


; I include all the lemmas that were proved during the talk
(include-book "lemmas")

(defun n-clockwise (from n)
  (mod (+ from 1) n))

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

(defun n-across (from n)
  (mod (+ from (/ n 2)) n))

(defthm force-case-split
  (implies (and (integerp dest)
                (integerp from)
                (<= 0 dest)
                (<= 0 from))
            (iff (not (equal dest from))
                  (or (< (+ dest (- from)) 0)
                      (< 0 (+ dest (- from))))))
  :rule-classes nil)

(defthm <=-=-<-or-=
  (implies (and (acl2-numberp a)
                (acl2-numberp b)
                )
           (equal (<= a b)
                  (or (< a b)
                      (= a b))))
  :rule-classes nil)



(defun n-go-to-node (dest from n)
  (declare (xargs :measure (min (nfix (mod (- dest from) n))
                                (nfix (mod (- from dest) n)))
                  :hints 
                  (("GOAL" 
                    :use ((:instance force-case-split)
                          (:instance <=-=-<-or-= (a dest) (b (+ -1 n)))
                          (:instance <=-=-<-or-= (a from) (b (+ -1 n)))
                          (:instance mod-+-n/2-pos (x (+ (- dest) from)))
                          )
                    :in-theory (disable PREFER-POSITIVE-ADDENDS-<
                                        mod-+-n/2-pos 
                                        ))
                   ("Subgoal 808.4" :cases ((<= 0 (+ -1 from))
                                            (< (+ -1 from) 0))))
                  ))
  (cond ((or (not (integerp dest)) 
            (< dest 0) 
            (< (- n 1) dest) 
            (not (integerp from)) 
            (< from 0) 
            (< (- n 1) from) 
            (not (integerp n)) 
            (<= n 0) 
            (not (equal (mod n 4) 0))) 
        nil) 
        ((equal (- dest from) 0) nil)
        ((and (< 0 (mod (- dest from) n))
              (<= (mod (- dest from) n) (/ n 4))) 
         (cons from 
               (n-go-to-node dest (n-clockwise from n) n)))
        ((and (<= (- n (/ n 4)) (mod (- dest from) n))
              (< (mod (- dest from) n) n))
         (cons from 
	       (n-go-to-node dest (n-counter-clockwise from n) n)))
        (t
         (cons from 
               (n-go-to-node dest (n-across from n) n)))))