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