; (certify-book "script")

; A Proof of the Correctness of Dijkstra's Shortest Path Algorithm in
; ACL2

; J Strother Moore and Qiang Zhang
; Department of Computer Sciences
; Univesity of Texas at Austin

; October, 2004

; See the paper ``Dijkstra's Shortest Path Algorithm Verified with ACL2''
; by the authors for a description of this script.

; Historical Notes: The first version of this proof was completed by
; Moore in September, 2003.  See /u/moore/shortest-path/dsp6.lisp.
; That file contained 92 defthms, 35 :hints, about 75 clause
; identifiers like "Goal" and "Subgoal" (some occur in comments), and
; 40 :use hints.  In order to learn ACL2, Zhang was given the task by
; Moore, first, to discover (independently) a proof (given the
; invariant), and, then, to clean it up.

; Zhang finished his first proof in December, 2003, using ACL2 Version
; 2.7.  In October, 2004, he cleaned up the proof, eliminating some of
; his hints.  This file is his second proof script.  In February,
; 2005, the authors wrote the paper above and in doing so renamed some
; of Zhang's functions and theorems.

; The current file contains 39 defuns, 125 defthms, 51 hints, 23 of
; which are :use hints mentioning 31 lemma instances.


(in-package "ACL2")

(defun del (x y)
  (if (endp y) nil
    (if (equal x (car y))
	(cdr y)
      (cons (car y) (del x (cdr y))))))

(defun memp (e x)
  (if (endp x) nil
    (or (equal e (car x))
	(memp e (cdr x)))))

(defun setp (s)
  (cond ((endp s) t)
	((memp (car s) (cdr s)) nil)
	(t (setp (cdr s)))))

(defun my-union (s1 s2)
  (cond ((endp s1) s2)
	((memp (car s1) s2)
	 (my-union (cdr s1) s2))
	(t (cons (car s1)
		 (my-union (cdr s1) s2)))))

(defun my-subsetp (s1 s2)
  (cond ((endp s1) t)
	(t (and (memp (car s1) s2)
		(my-subsetp (cdr s1) s2)))))

(defun infinitep (x) (null x)) 

(defun lt (x y)
  (cond ((infinitep x) nil)
	((infinitep y) t)
	(t (< x y))))

(defun plus (x y)
  (cond ((or (infinitep x)
	     (infinitep y))
	 nil)
	(t (+ x y))))

(defun edge-listp (lst)
  (cond ((endp lst) (equal lst nil))
	((and (consp (car lst))
	      (rationalp (cdar lst))
	      (<= 0 (cdar lst))
	      (not (assoc (caar lst)
			  (cdr lst))))
	 (edge-listp (cdr lst)))
	(t nil)))

(defun graphp (g)
  (cond ((endp g) (equal g nil))
	((and (consp (car g))
	      (edge-listp (cdar g)))
	 (graphp (cdr g)))
	(t nil)))

(defun cons-set (e s)
  (if (memp e s) s
    (cons e s)))

(defun all-nodes (g)
  (cond ((endp g) nil)
	(t (cons-set (caar g)
		     (my-union (strip-cars (cdar g))
			       (all-nodes (cdr g)))))))

(defun nodep (n g) (memp n (all-nodes g)))

(defun neighbors (n g)
  (strip-cars (cdr (assoc n g))))

(defun pathp-aux (path g)
  (cond ((endp path) nil)
	((endp (cdr path))
	 (nodep (car path) g))
	(t (and (memp (cadr path)
		     (neighbors (car path) g))
		(pathp-aux (cdr path) g)))))

(defun pathp (path g)
  (and (true-listp path)
       (pathp-aux path g)))

(defun edge-len (a b g)
  (cdr (assoc b (cdr (assoc a g)))))

(defun path-len (path g)
  (cond ((endp path) nil)
	((endp (cdr path))
	 (if (nodep (car path) g) 0 nil))
	(t (plus (edge-len (car path) (cadr path) g)
		 (path-len (cdr path) g)))))

(defun path (n pt) (cdr (assoc n pt)))

(defun d (n pt g)
  (path-len (path n pt) g))

(defun choose-next (ts pt g)
  (cond ((endp ts) '(non-node))
	((endp (cdr ts)) (car ts))
	((lt (d (car ts) pt g)
	     (d (choose-next (cdr ts) pt g) pt g))
	 (car ts))
	(t (choose-next (cdr ts) pt g))))

(defun reassign (u v-lst pt g)
  (cond ((endp v-lst) pt)
	(t (let* ((v (car v-lst))
		  (w (edge-len u v g)))
	     (cond ((lt (plus (d u pt g) w)
			(d v pt g))
		    (cons (cons v (append (path u pt) (list v)))
			  (reassign u (cdr v-lst) pt g)))
		   (t (reassign u (cdr v-lst) pt g)))))))

(defun dsp (ts pt g)
  (cond ((endp ts) pt)
	(t (let ((u (choose-next ts pt g)))
	     (dsp (del u ts)
		  (reassign u (neighbors u g) pt g)
		  g)))))

(defun dijkstra-shortest-path (a b g)
  (let ((p (dsp (all-nodes g)
		(list (cons a (list a))) g)))
    (path b p)))

;===================================================================
(defun pathp-from-to (p a b g)
  (and (pathp p g)
       (equal (car p) a)
       (equal (car (last p)) b)))

(defthm pathp-from-to-corollary
  (implies (pathp-from-to p a b g)
           (and (pathp p g)
                (equal (car p) a)
                (equal (car (last p)) b))))

(defun pt-propertyp (a pt g)
  (if (endp pt) t
    (and (or (null (cdar pt))
             (pathp-from-to (cdar pt) a (caar pt) g))
	 (pt-propertyp a (cdr pt) g))))

(defthm pathp-from-to-path-1 ; [Custom]
  (implies (and (pt-propertyp a pt g)
		(path u pt))
	   (pathp-from-to (path u pt) a u g))
  :rule-classes :forward-chaining)

(defthm pathp-from-to-path-2 ; [Custom]
  (implies (and (pt-propertyp a pt g)
		(path u pt))
	   (pathp-from-to (path u pt)
			      a u g)))

(defun lte (n1 n2)
  (not (lt n2 n1)))

(defun shorterp (p1 p2 g)
  (lte (path-len p1 g)
       (path-len p2 g)))

(defun confinedp (p fs)
  (if (endp p) t
    (if (endp (cdr p)) t
      (and (memp (car p) fs)
	   (confinedp (cdr p) fs)))))

(defun-sk shortest-confined-pathp (a b p fs g)
  (forall path (implies (and (pathp-from-to path a b g)
			     (confinedp path fs))
			(shorterp p path g))))

  
(defun-sk shortest-pathp (a b p g)
  (forall path (implies (pathp-from-to path a b g)
			(shorterp p path g))))

(defun ts-propertyp (a ts fs pt g)
  (if (endp ts) t
    (and (shortest-confined-pathp a (car ts) (path (car ts) pt) fs g)
	 (confinedp (path (car ts) pt) fs)
	 (ts-propertyp a (cdr ts) fs pt g))))

(defun fs-propertyp (a fs fs0 pt g)
  (if (endp fs) t
    (and (shortest-pathp a (car fs) (path (car fs) pt) g)
	 (confinedp (path (car fs) pt) fs0)
	 (fs-propertyp a (cdr fs) fs0 pt g))))

(defun comp-set (ts s)
  (if (endp s) nil
    (if (memp (car s) ts)
	(comp-set ts (cdr s))
      (cons (car s) (comp-set ts (cdr s))))))

(defun invp (ts pt g a)
  (let ((fs (comp-set ts (all-nodes g))))
    (and (ts-propertyp a ts fs pt g)
	 (fs-propertyp a fs fs pt g)
	 (pt-propertyp a pt g))))

(defthm prop-path-nil ; [Custom]
  (ts-propertyp a s nil (list (cons a (list a))) g))

(defthm comp-set-subset
  (implies (my-subsetp s1 s2)
           (not (comp-set s2 s1))))

(defthm subsetp-cons
  (implies (my-subsetp x y)
           (my-subsetp x (cons e y))))

(defthm subsetp-x-x
  (my-subsetp x x))

(defthm comp-set-id
  (equal (comp-set s s) nil))

(defthm invp-0 ; [Custom]
  (implies (nodep a g)
	   (invp (all-nodes g) (list (cons a (list a))) g a)))

;====================================================================
(defthm subset-union
  (implies (or (my-subsetp s1 s2)
               (my-subsetp s1 s3))
           (my-subsetp s1 (my-union s2 s3))))

(defthm memp-subset-memp-temp
  (implies (and (memp a s)
                (my-subsetp s r))
           (memp a r)))

(defthm neighbor-implies-nodep
  (implies (memp v (neighbors u g))
           (memp v (all-nodes g))))

(defthm paths-table-reassign-lemma2
  (implies (and (pathp p g)
                (memp v (neighbors (car (last p)) g)))
           (pathp (append p (list v)) g))
  :hints (("Goal" :in-theory (disable neighbors))))

(defthm car-append
  (implies (and (true-listp p) p)
           (equal (car (append p lst))
                  (car p))))

(defthm last-append
  (equal (car (last (append p (list v))))
         v))

(defthm paths-table-reassign-lemma4 ; [Custom]
  (implies (and (pt-propertyp a pt g)
                (path u pt)
                (graphp g)
                (memp v (neighbors u g)))
           (pathp-from-to (append (path u pt) (list v))
                         a v g))
  :hints (("Goal" :in-theory (disable neighbors))))

(defthm path-len-implies-not-nil
  (implies (path-len (path u pt) g)
           (path u pt)))

(defthm edge-len-implies-neighbors
  (implies (edge-len u v g)
           (memp v (neighbors u g))))

(defthm pt-propertyp-reassign ; [Custom]
  (implies (and (pt-propertyp a pt g)
                (graphp g)
		(my-subsetp v-lst (all-nodes g)))
	   (pt-propertyp a (reassign u v-lst pt g) g))
  :hints (("Goal" :in-theory (disable path edge-len neighbors))))

;=====================================================================
(defthm shortest-pathp-corollary
  (implies (and (shortest-pathp a b p g)
                (pathp-from-to path a b g))
           (shorterp p path g))
  :hints (("Goal" :use shortest-pathp-necc)))

(defthm shortest-implies-unchanged-lemma1 ; [Custom]
  (equal (path v (cons (cons u path) pt))
         (if (equal v u) path
           (path v pt))))

(defthm memp-implies-memp-union-1
    (implies (memp u s1)
             (memp u (my-union s1 s2))))

(defthm memp-implies-memp-union-2
    (implies (memp u s2)
             (memp u (my-union s1 s2))))

(defthm not-memp-edge-len-lemma
  (implies (assoc v alst)
           (memp v (strip-cars alst))))

(defthm not-memp-edge-len
  (implies (not (memp v (all-nodes g)))
           (not (edge-len a v g))))

(defthm path-len-append
  (implies (pathp p g)
           (equal (path-len (append p (list v)) g)
                  (plus (path-len p g)
                        (edge-len (car (last p)) v g))))
  :hints (("Goal" :in-theory (disable neighbors edge-len))))

(defthm pathp-implies-true-listp
  (implies (pathp p g)
           (true-listp p)))

(defthm shortest-implies-unchanged ; [Custom]
  (implies (and (shortest-pathp a v (path v pt) g)
                (pt-propertyp a pt g)
                (graphp g)
                (nodep v g))
           (equal (path v (reassign u v-lst pt g))
                  (path v pt)))
  :hints (("Goal" 
           :in-theory (disable path edge-len neighbors pathp
                               shortest-pathp))
          ("Subgoal *1/2" 
           :use ((:instance path-len-implies-not-nil)
                                (:instance pathp-from-to-corollary
                                           (p (path u pt)) (b u))
				(:instance shortest-pathp-corollary
                                           (path (append (path u pt) (list v)))
                                           (b v) (p (path v pt)))))))
;=====================================================================
(defthm fs-propertyp-memp ; [Custom]
  (implies (and (fs-propertyp a fs s pt g)
		(memp v fs))
	   (and (shortest-pathp a v (path v pt) g)
		(confinedp (path v pt) s))))

(defthm fs-propertyp-memp-lemma ; [Custom]
  (implies (and (my-subsetp fs (all-nodes g))
		(fs-propertyp a fs s pt g)
		(pt-propertyp a pt g)
                (graphp g)
		(memp v fs))
	   (equal (path v (reassign u (neighbors u g) pt g))
		  (path v pt)))		  
  :hints (("Goal" :in-theory (disable neighbors path shortest-pathp))))

(defthm fs-propertyp-choose-next-lemma1 ; [Custom]
  (implies (and (fs-propertyp a fs s pt g)
		(pt-propertyp a pt g)
                (graphp g)
		(my-subsetp fs (all-nodes g)))
	   (fs-propertyp a fs s (reassign u (neighbors u g) pt g) g))
  :hints (("Goal" :in-theory (disable neighbors path shortest-pathp))))

(defthm fs-propertyp-choose-lemma2 ; [Custom]
  (implies (and (fs-propertyp a fs s pt g)
		(my-subsetp fs (all-nodes g))
		(confinedp (path u pt) s)
		(pt-propertyp a pt g)
		(nodep u g)
                (graphp g)
		(shortest-pathp a u (path u pt) g))
	   (fs-propertyp a (cons u fs) s
			 (reassign u (neighbors u g) pt g)
			 g))
  :hints (("Goal" :in-theory (disable path neighbors))))

(defthm fs-propertyp-choose-lemma3 ; [Custom]
  (implies (and (my-subsetp s fs)
		(my-subsetp fs (all-nodes g))
		(pt-propertyp a pt g)
		(fs-propertyp a fs ss pt g))
	   (fs-propertyp a s ss pt g))
  :hints (("Goal" :in-theory (disable shortest-pathp path))))

(defthm fs-propertyp-choose-lemma4-lemma ; [Custom]
  (implies (and (my-subsetp s ss)
		(confinedp p s))
	   (confinedp p ss)))

(defthm fs-propertyp-choose-lemma4 ; [Custom]
  (implies (and (my-subsetp s ss)
		(fs-propertyp a fs s pt g))
	   (fs-propertyp a fs ss pt g)))

(defun find-partial-path (p s)
  (if (endp p) nil
    (if (memp (car p) s)
	(cons (car p) (find-partial-path (cdr p) s))
      (list (car p)))))

(defthm edge-listp-values-positive
  (implies (and (edge-listp a)
                (cdr (assoc-equal b a)))
           (<= 0 (cdr (assoc-equal b a))))
  :rule-classes :linear)

(defthm graph-weight-nonneg
  (implies (and (graphp g)
		(edge-len a b g))
	   (<= 0 (edge-len a b g)))
  :rule-classes :linear)

(defthm graph-path-weight-nonneg
  (implies (and (graphp g)
		(path-len p g))
	   (<= 0 (path-len p g)))
  :rule-classes :linear
  :hints (("Goal" :in-theory (disable edge-len))))

(defthm edge-len-implies-nodep
  (implies (edge-len a b g)
           (memp a (all-nodes g))))

(defthm partial-path-shorterp
  (implies (graphp g)
	   (shorterp (find-partial-path p s)
			 p g))
  :hints (("Goal" :induct (find-partial-path p s)
           :in-theory (disable edge-len))))

(defthm notnodep-necc
  (implies (not (nodep a g))
	   (not (neighbors a g))))

(defthm pathp-implies-car-nodep
  (implies (pathp p g)
           (memp (car p) (all-nodes g))))

(defthm pathp-partial-path
  (implies (pathp p g)
           (and (pathp-from-to (find-partial-path p s) (car p)
                              (car (last (find-partial-path p s))) g)
                (confinedp (find-partial-path p s) s))))

(defthm shorterp-trans
  (implies (and (shorterp p1 p2 g)
                (shorterp p2 p3 g))
           (shorterp p1 p3 g)))

(defthm shorterp-by-partial-trans
  (implies (and (shorterp p (find-partial-path path s) g)
                (graphp g))
           (shorterp p path g))
  :hints (("Goal" :in-theory (disable shorterp))))

(defthm ts-propertyp-prop-lemma1 ; [Custom]
  (implies (and (ts-propertyp a ts fs pt g)
		(memp v ts))
	   (and (shortest-confined-pathp a v (path v pt) fs g)
		(confinedp (path v pt) fs)))
  :rule-classes ((:rewrite)(:forward-chaining)))

(defthm ts-propertyp-prop-lemma2 ; [Custom]
  (implies (and (pathp-from-to path a b g)
                (shortest-confined-pathp a b p fs g)
                (confinedp path fs))
	   (shorterp p path g))
  :hints (("Goal" :use shortest-confined-pathp-necc)))

(defthm ts-propertyp-prop ; [Custom]
  (implies (and (ts-propertyp a ts fs pt g)
		(confinedp path fs)
		(pathp-from-to path a v g)
		(memp v ts))
	   (and (shorterp (path v pt) path g)
		(confinedp (path v pt) fs)))
  :hints (("Goal" :in-theory (disable path shorterp pathp-from-to))))

(defthm shorterp-by-partial-and-choose-next ; [Custom]
  (implies (and (shorterp (path u pt) (path v pt) g)
		(memp v ts)
		(ts-propertyp a ts (comp-set ts (all-nodes g)) pt g)
		(pathp-from-to path a v g)
		(confinedp path (comp-set ts (all-nodes g))))
	   (shorterp (path u pt) path g))
  :hints (("Goal" :in-theory (disable path shorterp))))

(defthm choose-next-shorterp-other ; [Custom]
  (implies (memp v ts)
           (shorterp (path (choose-next ts pt g) pt)
                    (path v pt) g)))

(defthm not-comp-set-id
  (implies (memp v all)
           (iff (memp v (comp-set ts all))
                (not (memp v ts)))))

(defthm find-partial-path-last-memp
  (implies (and (memp (car (last p)) ts)
		(pathp p g)
		(my-subsetp ts (all-nodes g)))
	   (memp (car (last (find-partial-path p (comp-set ts (all-nodes g)))))
		ts)))

(defthm choose-next-shortest-lemma ; [Custom]
  (implies (consp ts)
	   (memp (choose-next ts pt g) ts)))

(defthm choose-next-shortest ; [Custom]
  (implies (and (graphp g)
		(consp ts)
		(my-subsetp ts (all-nodes g))
		(invp ts pt g a))
	   (shortest-pathp a (choose-next ts pt g)
                           (path (choose-next ts pt g) pt) g))
  :hints
  (("Goal" :in-theory (disable shorterp path pathp)
    :use ((:instance
           pathp-partial-path
           (p (shortest-pathp-witness a (choose-next ts pt g)
                                      (path (choose-next ts pt g) pt)
                                      g))
           (s (comp-set ts (all-nodes g))))
          (:instance
           shorterp-by-partial-and-choose-next
           (u (choose-next ts pt g))
           (path (find-partial-path 
                  (shortest-pathp-witness a 
                                          (choose-next ts pt g)
                                          (path (choose-next ts pt g) pt)
                                          g)
                  (comp-set ts (all-nodes g))))
           (v (car (last (find-partial-path 
                          (shortest-pathp-witness a (choose-next ts pt g)
                                                  (path (choose-next ts pt g) 
                                                        pt)
                                                  g)
                          (comp-set ts (all-nodes g)))))))))))

(defthm choose-next-confinedp ; [Custom]
  (implies (and (invp ts pt g a)
		(consp ts)
		(my-subsetp ts (all-nodes g)))
	   (confinedp (path (choose-next ts pt g) pt)
			      (comp-set ts (all-nodes g))))
  :hints (("Goal" :in-theory (disable path))))

(defthm subsetp-comp-set-all
  (my-subsetp (comp-set ts all) all))

(defthm subsetp-del
  (my-subsetp (del u ts) ts))

(defthm cons-subsetp-comp-set-del-lemma
  (my-subsetp (comp-set ts all)
	      (comp-set (del u ts) all)))

(defthm subsetp-comp-set-del-lemma1
  (implies (my-subsetp s1 (cons v s2))
	   (my-subsetp s1
		       (list* v u s2))))

(defthm subsetp-comp-set-del-lemma2
  (implies (and (memp v ts)
                (not (equal v u)))
           (memp v (del u ts))))

(defthm subsetp-comp-set-del
  (implies (and (setp ts)
		(setp all))
	   (my-subsetp (comp-set (del u ts) all)
		       (cons u (comp-set ts all)))))

(defthm edge-listp-prop
  (implies (and (edge-listp lst)
		(not (assoc u lst)))
	   (not (memp u (strip-cars lst)))))

(defthm edge-listp-implies-setp
  (implies (edge-listp lst)
	   (setp (strip-cars lst))))

(defthm not-memp-union
  (implies (and (not (memp u s1))
		(not (memp u s2)))
	   (not (memp u (my-union s1 s2)))))

(defthm setp-union
  (implies (and (setp s1)
		(setp s2))
	   (setp (my-union s1 s2))))

(defthm setp-all-nodes
  (implies (graphp g)
           (setp (all-nodes g))))

(defthm memp-subset-memp
  (implies (and (my-subsetp s r)
                (memp a s))
           (memp a r)))

(defthm neighbors-subsetp-all-nodes
  (my-subsetp (neighbors u g)
              (all-nodes g)))

(defthm fs-propertyp-choose ; [Custom]
  (implies (and (invp ts pt g a)
		(my-subsetp ts (all-nodes g))
		(graphp g)
		(consp ts)
		(setp ts))
	   (let ((u (choose-next ts pt g)))
	     (fs-propertyp a (comp-set (del u ts)
				       (all-nodes g))
			   (comp-set (del u ts) (all-nodes g))
			   (reassign u (neighbors u g) pt g)
			   g)))
  :hints (("Goal" :in-theory (disable fs-propertyp-choose-lemma3
				      fs-propertyp-choose-lemma4
				      path neighbors shortest-pathp
				      fs-propertyp)
	   :use ((:instance fs-propertyp-choose-lemma4
			    (fs (comp-set (del (choose-next ts pt g) ts)
					  (all-nodes g)))
			    (s (comp-set ts (all-nodes g)))
			    (ss (comp-set (del (choose-next ts pt g) ts)
					  (all-nodes g)))
			    (pt (reassign (choose-next ts pt g)
					  (neighbors (choose-next ts pt g) g)
					  pt g)))
		 (:instance fs-propertyp-choose-lemma3
			    (s (comp-set (del (choose-next ts pt g) ts)
					  (all-nodes g)))
			    (fs (cons (choose-next ts pt g)
				      (comp-set ts (all-nodes g))))
			    (ss (comp-set ts (all-nodes g)))
			    (pt (reassign (choose-next ts pt g)
					  (neighbors (choose-next ts pt g) g)
					  pt g)))))))                 
;=====================================================================
(defthm neighbor-implies-edge-len
  (implies (and (graphp g)
                (memp v (neighbors u g)))
           (edge-len u v g)))

(defthm pathp-implies-path-len
  (implies (and (graphp g)
		(pathp p g))
		(path-len p g))
  :hints (("Goal" :in-theory (disable neighbors edge-len))))

(defthm path-pt-iff-path-len ; [Custom]
  (implies (and (graphp g)
                (pt-propertyp a pt g))
           (iff (path u pt)
                (path-len (path u pt) g))))

(defthm reassign-path ; [Custom]
  (implies (not (memp v v-lst))
	   (equal (path v (reassign u v-lst pt g))
		  (path v pt))))

(defthm shorterp-reassign-append ; [Custom]
  (implies (and (pt-propertyp a pt g)
                (graphp g)
                (path u pt)
                (memp v v-lst))
           (shorterp (path v (reassign u v-lst pt g))
                    (append (path u pt) (list v)) g))
  :hints (("Goal" :in-theory (disable edge-len path pathp-from-to-path-1))
          ("Subgoal *1/3" 
           :use ((:instance pathp-from-to-corollary
                            (p (path u pt)) (b u))))))
           
(defun find-last-next-path (p)
  (if (or (endp p) (endp (cdr p))) nil
    (cons (car p) (find-last-next-path (cdr p)))))

(defun last-node (p)
  (car (last (find-last-next-path p))))

(defthm shorterp-reassign-lemma ; [Custom]
  (implies (and (path-len (path u pt) g)
                (pt-propertyp a pt g))
           (and (pathp (path u pt) g)
                (equal (car (path u pt)) a)
                (equal (car (last (path u pt))) u))))

(defthm shorterp-reassign ; [Custom]
  (implies (pt-propertyp a pt g)
           (shorterp (path v (reassign u v-lst pt g))
                    (path v pt) g))
  :hints (("Goal" :in-theory (disable path edge-len neighbors))))                          

(defthm true-listp-path ; [Custom]
  (implies (pt-propertyp a pt g)
	   (true-listp (path u pt))))

(defthm pathp-from-to-append ; [Custom]
  (implies (and (pt-propertyp a pt g)
		(path w pt)
		(memp v (neighbors w g)))
	   (pathp-from-to (append (path w pt)
				 (list v))
			 a v g))
  :hints (("Goal" :in-theory (disable neighbors path))))

(defthm confinedp-append
  (implies (and (confinedp p s)
		(memp (car (last p)) s))
	   (confinedp (append p (list v)) s)))

(defthm shorterp-than-append-fs ; [Custom]
  (implies (and (shortest-confined-pathp a v (path v pt) s g)
		(fs-propertyp a fs s pt g)
		(my-subsetp fs s)
		(path w pt)
		(pt-propertyp a pt g)
		(memp w fs))
	   (shorterp (path v pt)
		    (append (path w pt) (list v)) g))
  :rule-classes nil
  :hints (("Goal" :use ((:instance ts-propertyp-prop-lemma2
                                   (b v) (p (path v pt)) (fs s)
                                   (path (append (path w pt) (list v)))))
           :in-theory (disable path shortest-confined-pathp pathp))))

(defthm path-length
  (implies (and (pathp p g)
                (not (equal (car p)
                            (car (last p)))))
           (<= 2 (len p)))
  :rule-classes :linear)

(defthm pathp-find-last-next 
  (implies (and (pathp p g)
		(<= 2 (len p)))
	   (and (pathp (find-last-next-path p) g)
		(memp (car (last p)) 
		     (neighbors (car (last (find-last-next-path p))) g))))
  :hints (("Goal" :in-theory (disable neighbors))))

(defthm find-last-implies-all-in
  (implies (and (find-last-next-path p)
		(confinedp p fs))
	   (memp (car (last (find-last-next-path p))) fs)))

(defthm pathp-from-to-implies-all-path
  (implies (and (pathp-from-to p a v g)
		(not (equal a v))
		(confinedp p fs))
	   (and (memp v (neighbors (last-node p) g))
                (pathp-from-to (find-last-next-path p) a (last-node p) g)
		(memp (last-node p) fs)))
  :hints (("Goal" :in-theory (disable pathp neighbors))))
		       
(defthm path-len-implies-pathp
  (implies (and (path-len p g)
                (true-listp p))
           (pathp p g))
  :hints (("Goal" :in-theory (disable edge-len neighbors))))

(defthm shorterp-and-pathp-implies-pathp
  (implies (and (graphp g)
		(shorterp p1 p2 g)
		(true-listp p1)
		(pathp p2 g))
	   (pathp p1 g))
  :rule-classes nil
  :hints (("Goal" :in-theory (disable pathp))))

(defthm shorterp-implies-append-shorterp
  (implies (and (shorterp p1 p2 g)
		(graphp g)
		(true-listp p1)
		(equal (car (last p1))
		       (car (last p2)))
		(pathp p2 g))
	   (shorterp (append p1 (list v))
		    (append p2 (list v)) g))
  :hints (("Goal" :use shorterp-and-pathp-implies-pathp)))

(defthm path-pt-implies-path-last-node ; [Custom]
  (implies (and (pt-propertyp a pt g)
		(pathp (path u pt) g))
	   (equal (car (last (path u pt))) u)))

(defthm last-node-lemma1 ; [Custom]
  (implies (and (graphp g)
		(pt-propertyp a pt g)
		(pathp-from-to p a v g)
		(not (equal a v))
		(shortest-pathp a (last-node p) (path (last-node p) pt) g))
	   (shorterp (append (path (last-node p) pt) (list v)) 
		    (append (find-last-next-path p) (list v)) g))
  :hints (("Goal" :in-theory (disable shortest-pathp shorterp path pathp)
	   :use ((:instance shorterp-and-pathp-implies-pathp
                            (p1 (path (car (last (find-last-next-path p))) pt))
                            (p2 (find-last-next-path p)))
                 (:instance shortest-pathp-corollary
                            (b (car (last (find-last-next-path p))))
                            (p (path (car (last (find-last-next-path p))) pt))
                            (path (find-last-next-path p)))))))

(defthm last-node-lemma2 ; [Custom]
  (implies (and (equal (car (last p)) v)
		(pathp p g))
	   (equal (append (find-last-next-path p) (list v))
		  p)))

(defthm last-node-lemma ; [Custom]
  (implies (and (graphp g)
		(pt-propertyp a pt g)
		(pathp-from-to p a v g)
		(not (equal a v))
		(shortest-pathp a (last-node p) (path (last-node p) pt) g))
	   (shorterp (append (path (last-node p) pt) (list v))
		    p g))
  :hints (("Goal" :use ((:instance last-node-lemma1)
			(:instance last-node-lemma2))
	   :in-theory (disable shorterp))))

(defthm memp-not-car-implies-memp
  (implies (and (memp v (cons u fs))
		(not (equal v u)))
	   (memp v fs)))

(defthm fs-propertyp-implies-pathp ; [Custom]
  (implies (and (graphp g)
		(fs-propertyp a fs s pt g)
		(memp w fs)
		(pathp-from-to p2 a w g))
	   (path w pt))
  :hints (("Goal" :in-theory (disable path fs-propertyp-memp shortest-pathp
                                      pathp-from-to)
	   :use ((:instance shortest-pathp-corollary
			    (b w) (p (path w pt))
			    (path p2))
		 (:instance fs-propertyp-memp
			    (v w)))))
  :rule-classes nil)

(defthm ts-propertyp-lemma2-1 ; [Custom]
  (implies (and (shortest-confined-pathp a v (path v pt) fs g)
		(graphp g)
		(fs-propertyp a fs fs pt g)
		(pathp-from-to p a v g)
		(not (equal a v))
		(path u pt)
		(shortest-pathp a u (path u pt) g)
		(confinedp p (cons u fs))
		(pt-propertyp a pt g))
	   (shorterp (path v (reassign u (neighbors u g) pt g)) p g))
  :hints (("Goal"
	   :cases ((equal (last-node p) u)))
	  ("Subgoal 2" :in-theory (disable path neighbors shortest-confined-pathp 
					   shorterp shortest-pathp memp-not-car-implies-memp
					   fs-propertyp-memp pathp-from-to last-node)
	   :use ((:instance shorterp-trans
			    (p1 (path v (reassign u (neighbors u g) pt g)))
			    (p2 (path v pt))
			    (p3 (append (path (last-node p) pt) (list v))))
                 (:instance shorterp-trans
			    (p1 (path v (reassign u (neighbors u g) pt g)))
			    (p2 (append (path (last-node p) pt) (list v)))
			    (p3 p))
		 (:instance fs-propertyp-memp
			    (s fs)
			    (v (last-node p)))
		 (:instance memp-not-car-implies-memp
			    (v (last-node p)))
		 (:instance fs-propertyp-implies-pathp
			    (s fs)
			    (w (last-node p))
			    (p2 (find-last-next-path p)))
		 (:instance shorterp-than-append-fs
			    (s fs) (w (last-node p)))))
	  ("Subgoal 1" :in-theory (disable path neighbors shortest-confined-pathp
					   last-node shorterp shortest-pathp pathp-from-to)
	   :use ((:instance shorterp-trans
			    (p1 (path v (reassign u (neighbors u g) pt g)))
			    (p2 (append (path u pt) (list v)))
			    (p3 p))))))
;=====================================================================
(defun find-partial-path-to-u (p u)
  (cond ((not (memp u p)) nil)
	((equal (car p) u) (list u))
	(t (cons (car p)
		 (find-partial-path-to-u (cdr p) u)))))

(defthm pathp-implies-path-to-u-pathp
  (implies (and (memp u p)
		(pathp p g))
	   (pathp-from-to (find-partial-path-to-u p u) (car p) u g)))

(defthm not-memp-implies-confinedp
  (implies (and (confinedp p (cons u fs))
		(not (memp u p)))
	   (confinedp p fs)))

(defthm nil-shorterp-than-nil
  (implies (and (shorterp p1 p2 g)
		(graphp g)
		(not p1))
	   (not (pathp p2 g))))

(defthm shortest-pathp-nil-implies-lemma
  (implies (and (shortest-pathp a u p1 g)
		(not p1)
		(graphp g)
		(equal (car p2) a)
		(pathp p2 g))
	   (not (memp u p2)))
  :hints (("Goal" :in-theory (disable pathp shorterp shortest-pathp pathp-implies-path-to-u-pathp)
	   :use ((:instance pathp-implies-path-to-u-pathp
		           (p p2))
		 (:instance nil-shorterp-than-nil
			    (p2 (find-partial-path-to-u p2 u)))))))

(defthm ts-propertyp-lemma2-2 ; [Custom]
  (implies (and (shortest-confined-pathp a v (path v pt) fs g)
		(graphp g)
		(fs-propertyp a fs fs pt g)
		(pathp-from-to p a v g)
		(not (equal a v))
		(shortest-pathp a u (path u pt) g)
		(confinedp p (cons u fs))
		(pt-propertyp a pt g))
	   (shorterp (path v (reassign u (neighbors u g) pt g)) p g))
  :rule-classes nil
  :hints (("Goal" :cases ((path u pt)))
	  ("Subgoal 2" :in-theory (disable neighbors path pathp
                                           pathp-from-to
                                           path-pt-iff-path-len
					   shortest-pathp shorterp
					   shortest-confined-pathp)
	   :use ((:instance shorterp-trans
                            (p1 (path v (reassign u (neighbors u g) pt g)))
                            (p2 (path v pt))
                            (p3 p))
                 (:instance ts-propertyp-prop-lemma2
			    (b v) (p (path v pt))
			    (path p))))
	  ("Subgoal 1" :use ts-propertyp-lemma2-1)))

(defthm shortest-pathp-list-a
  (implies (graphp g)
           (shortest-pathp a a (list a) g)))

(defthm path-a-pt ; [Custom]
  (implies (and (pt-propertyp a pt g)
		(graphp g)
		(nodep a g)
		(equal (path a pt) (list a)))
	   (equal (path a (reassign u v-lst pt g))
		  (path a pt)))
  :hints (("Goal" :use ((:instance shortest-implies-unchanged
                                   (v a))))))

(defthm ts-propertyp-lemma2-3 ; [Custom]
  (implies (and (shortest-confined-pathp a v (path v pt) fs g)
		(graphp g)
		(fs-propertyp a fs fs pt g)
		(nodep a g)
		(pathp-from-to p a v g)
		(confinedp p (cons u fs))
		(shortest-pathp a u (path u pt) g)
		(pt-propertyp a pt g)
		(equal (path a pt) (list a)))
	   (shorterp (path v (reassign u (neighbors u g) pt g)) p g))
  :rule-classes nil
  :hints (("Goal" :cases ((equal a v)))
	  ("Subgoal 2" :use ts-propertyp-lemma2-2)
	  ("Subgoal 1" :in-theory (disable path neighbors pathp
					   shortest-pathp
					   shortest-confined-pathp))))

(defthm ts-propertyp-lemma2 ; [Custom]
  (implies (and (shortest-confined-pathp a v (path v pt) fs g)
		(graphp g)
		(nodep a g)
		(equal (path a pt) (list a))
		(fs-propertyp a fs fs pt g)
		(shortest-pathp a u (path u pt) g)
		(pt-propertyp a pt g))
	   (shortest-confined-pathp a v (path v (reassign u (neighbors u g)
							 pt g)) 
				   (cons u fs) g))
  :hints (("Goal" :in-theory (disable reassign path neighbors shortest-pathp shortest-confined-pathp)
	   :expand ((shortest-confined-pathp a v (path v (reassign u (neighbors u g)
							 pt g)) 
					    (cons u fs) g))
	   :use ((:instance ts-propertyp-lemma2-3
			   (p (SHORTEST-CONFINED-PATHP-WITNESS A V
                                   (PATH V (REASSIGN U (NEIGHBORS U G) PT G))
                                   (CONS U FS)
                                   G)))))))

(defthm ts-propertyp-lemma3-1
  (implies (confinedp p fs)
	   (confinedp p (cons u fs))))

(defthm ts-propertyp-lemma3-2 ; [Custom]
  (implies (and (pt-propertyp a pt g)
                (confinedp (path u pt) fs))
	   (confinedp (append (path u pt) (list v))
			      (cons u fs))))

(defthm ts-propertyp-lemma3-3 ; [Custom]
  (implies (and (pt-propertyp a pt g)
                (confinedp (path v pt) fs)
                (confinedp (path u pt) fs))
	   (confinedp (path v (reassign u v-lst pt g)) 
			      (cons u fs)))
  :hints (("Goal" :in-theory (disable path))))

(defthm ts-propertyp-prop-lemma ; [Custom]
  (implies (and (ts-propertyp a ts fs pt g)
		(memp u ts))
	   (confinedp (path u pt) fs)))

(defthm ts-propertyp-lemma3 ; [Custom]
  (implies (and (pt-propertyp a pt g)
		(graphp g)
		(nodep a g)
		(equal (path a pt) (list a))
		(fs-propertyp a fs fs pt g)
		(ts-propertyp a ts fs pt g)
		(memp u ts)
		(shortest-pathp a u (path u pt) g))
	   (ts-propertyp a (del u ts) (cons u fs)
			 (reassign u (neighbors u g) pt g) g))
  :hints (("Goal" :in-theory (disable path neighbors nodep shortest-pathp
				      shortest-confined-pathp))
	  ("Subgoal *1/2'''" :induct (TS-PROPERTYP A TS2 (CONS TS1 FS)
						 (REASSIGN TS1 (NEIGHBORS TS1 G) PT G)
						 G))))
(defthm shortest-confined-pathp-subset
  (implies (and (shortest-confined-pathp a u p fs g)
                (my-subsetp s fs))		
	   (shortest-confined-pathp a u p s g))
  :hints (("Goal" :in-theory (disable shortest-confined-pathp shorterp)
	   :expand ((shortest-confined-pathp a u p s g))
	   :use ((:instance ts-propertyp-prop-lemma2
			    (b u) 
			    (path (shortest-confined-pathp-witness a u p s g)))))))

(defthm ts-propertyp-lemma1 ; [Custom]
  (implies (and (my-subsetp s fs)
		(my-subsetp fs s)
                (ts-propertyp a ts fs pt g))
	   (ts-propertyp a ts s pt g))
  :hints (("Goal" :in-theory (disable shortest-confined-pathp))))

(defthm not-memp-del
  (implies (setp ts)
	   (not (memp u (del u ts)))))

(defthm ts-propertyp-choose-next ; [Custom]
  (implies (and (invp ts pt g a)
		(my-subsetp ts (all-nodes g))
		(setp ts)
		(consp ts)
		(graphp g)
		(nodep a g)
		(equal (path a pt) (list a)))
	   (let ((u (choose-next ts pt g)))
	     (ts-propertyp a (del u ts) (comp-set (del u ts) (all-nodes g))
			   (reassign u (neighbors u g) pt g) g)))
  :hints (("Goal" :in-theory (disable neighbors path shortest-pathp)
	   :use ((:instance ts-propertyp-lemma1
			    (pt (reassign (choose-next ts pt g)
					  (neighbors (choose-next ts pt g) g)
					  pt g))
			    (ts (del (choose-next ts pt g) ts))
			    (s (comp-set (del (choose-next ts pt g) ts) (all-nodes g)))
			    (fs (cons (choose-next ts pt g)
				      (comp-set ts (all-nodes g)))))))))

(defthm invp-choose-next ; [Custom]
  (implies (and (invp ts pt g a)
		(my-subsetp ts (all-nodes g))
		(graphp g)
		(consp ts)
		(setp ts)
		(nodep a g)
		(equal (path a pt) (list a)))
	   (let ((u (choose-next ts pt g)))
	     (invp (del u ts)
		  (reassign u (neighbors u g) pt g)
		  g a)))
  :hints (("Goal" :in-theory (disable neighbors))))

(defthm del-subsetp
  (implies (my-subsetp ts s)
	   (my-subsetp (del u ts) s)))

(defthm del-true-listp 
  (implies (true-listp ts)
	   (true-listp (del u ts))))

(defthm del-noduplicates
  (implies (setp ts)
	   (setp (del u ts))))

(defthm path-a-pt-reassign ; [Custom]
  (implies (and (pt-propertyp a pt g)
		(graphp g)
		(nodep a g)
		(equal (path a pt) (list a)))
	   (equal (path a (reassign u v-lst pt g))
		  (list a)))
  :hints (("Goal" :in-theory (disable path)))) 

(defthm invp-last-lemma ; [Custom]
  (implies (and (invp ts pt g a)
		(my-subsetp ts (all-nodes g))
		(nodep a g)
		(equal (path a pt) (list a))
		(true-listp ts)
		(graphp g)
		(setp ts))
	   (invp nil (dsp ts pt g) g a))
  :hints (("Goal" :in-theory (disable path neighbors))))

(defthm true-listp-union
  (implies (and (true-listp lst1)
		(true-listp lst2))
	   (true-listp (my-union lst1 lst2))))

(defthm true-list-all-nodes
  (true-listp (all-nodes g)))

(defthm invp-last ; [Custom]
  (implies (and (nodep a g)
		(graphp g))
	   (invp nil (dsp (all-nodes g)
			 (list (cons a (list a)))
			 g) g a)))

(defthm main-lemma1 ; [Custom]
  (implies (and (invp nil pt g a)
		(nodep b g))
	   (shortest-pathp a b (path b pt) g))	
  :hints (("Goal" :in-theory (disable path shortest-pathp))))

(defthm main-lemma2 ; [Custom]
  (implies (and (invp nil pt g a)
		(nodep b g))
	   (or (null (path b pt))
	       (pathp-from-to (path b pt) a b g)))
  :hints (("Goal" :in-theory (disable path)))
  :rule-classes nil)

(defthm main-lemma3 ; [Custom]
  (implies (and (nodep a g)
		(nodep b g)
		(graphp g))
	   (or (null (dijkstra-shortest-path a b g))
	       (pathp-from-to (dijkstra-shortest-path a b g)
			     a b g)))
  :hints (("Goal" :use ((:instance main-lemma2
				   (pt (DSP (ALL-NODES G)
					    (LIST (LIST A A))
					    G))))))
  :rule-classes nil)

(defthm main-lemma4 ; [Custom]
  (implies (and (nodep a g)
		(nodep b g)
		(graphp g))
	   (shortest-pathp a b (dijkstra-shortest-path a b g) g))
  :hints (("Goal" :in-theory (disable shortest-pathp path))))

(defthm main-theorem ; [Custom]
  (implies (and (nodep a g)
		(nodep b g)
		(graphp g))
	   (let ((rho (dijkstra-shortest-path a b g)))
             (and (or (null rho)
                      (pathp-from-to rho a b g))
                  (shortest-pathp a b rho g))))
  :rule-classes nil
  :hints (("Goal" :use (main-lemma3 main-lemma4))))