#| Prelude for concurrency:
   Sequential processes communicating by shared 
   variables
   A preparation, e.g., for Peterson's algorithm 
   for mutual exclusion.

   Wim H. Hesselink, September 8, 2000
   September 2002, extended with elimination of ghost variables.
   October 2002, extended with relational specification. 

   Dept. of Computing Science | phone +31 50 3633933
   University of Groningen    |    or +31 50 3633939
   P.O.Box 800                | fax   +31 50 3633800
   9700 AV Groningen          | email: wim@cs.rug.nl
   The Netherlands            | http://www.cs.rug.nl/~wim
|#

(boot-strap nqthm) 

(defn putassoc (var w x)
      (if (nlistp x) (cons (cons var w) x)
          (if (equal var (caar x))
              (cons (cons var w) (cdr x))
              (cons (car x) (putassoc var w (cdr x))) ) ) )

(prove-lemma assoc-put (rewrite)
    (equal (assoc key (putassoc var w x))
           (if (equal key var) (cons var w)
               (assoc key x) ) ) )

(defn cleanalist (d x)
    (if (nlistp d) nil
        (cons (cons (car d) (cdr (assoc (car d) x)))
              (cleanalist (cdr d) x) ) ) )

(defn proper (x)
    (if (nlistp x) nil
        (cons (car x) (proper (cdr x))) ) )

(lemma strip-cars-cleanalist (rewrite)
    (equal (strip-cars (cleanalist d x))
           (proper d) ) 
    ((enable proper cleanalist)) )

(lemma assoc-cleanalist (rewrite)
    (equal (assoc var (cleanalist d x))
           (if (member var d)
               (cons var (cdr (assoc var x)))
               f ) )
    ((enable cleanalist)) )

(defn shared (d x)    (cleanalist d (cdr x)) )
(defn privstate (q x) (cdr (assoc q (car x))) )
(defn lookup (a x)    (cdr (assoc a x)))
    
(dcl apply (fun args))

(defn eval (flag x a)
    (if (equal flag 'list)
	(if (nlistp x) nil
	  (cons (eval t (car x) a)
		(eval 'list (cdr x) a) ) )
      (if (litatom x) (cdr (assoc x a))
	(if (nlistp x) x
	  (if (equal (car x) 'quote) (cadr x)
	    (apply (car x) (eval 'list (cdr x) a)) ) ) ) ) )

(defn view (d q x) ; part of the state visible to process q
   (append (shared d x) 
	   (list* (cons 'self q)
		  (privstate q x)) ) )

(defn putlocal (q var w x)
    (cons (putassoc q (putassoc var w (privstate q x))
                    (car x))
          (cdr x) ) )

(prove-lemma private-vars-putlocal (rewrite)
    (implies (not (equal p q)) 
             (equal (privstate q (putlocal p var w x))
                    (privstate q x) ) ) ) ; triv

(defn putglobal (q var w x)
    (cons (car x) (putassoc var w (cdr x))) )

(defn putgen (d q var w x)
    (if (member var d)
        (putglobal q var w x)
        (putlocal q var w x) ) )

(defn exe (d q cmd x)
    (cond ((nlistp cmd) x)
          ((nlistp (car cmd))
           (case (car cmd)
                 (put (putgen d q (cadr cmd) 
                              (eval t (caddr cmd) (view d q x))
                              x ))
                 (if (if (eval t (cadr cmd) (view d q x))
                         (exe d q (caddr cmd) x)
                         (exe d q (cadddr cmd) x) ))
                 (otherwise x) ) )
          (t (exe d q (cdr cmd) 
                  (exe d q (car cmd) x) )) ) )

(prove-lemma private-vars-exe (rewrite)
    (implies (not (equal p q)) 
             (equal (privstate q (exe d p cmd x))
                    (privstate q x) ) ) )

(defn pc (q x) (lookup 'pc (privstate q x)))

(defn exepc (d q cmd x)
    (exe d q (cdr (assoc (pc q x) cmd))
	 (putlocal q 'pc (add1 (pc q x)) x) ) )

(lemma private-vars-exepc (rewrite)
    (implies (not (equal p q)) 
             (equal (privstate q (exepc d p cmd x))
                    (privstate q x) ) ) 
    ((enable exepc private-vars-exe private-vars-putlocal)) )

(deftheory gen-conc-th 
   (putassoc assoc-put cleanalist proper strip-cars-cleanalist 
	     assoc-cleanalist shared privstate lookup view putlocal
	     private-vars-putlocal putglobal putgen pc ) )

#| Elimination of ghost variables, version Sept. 2002 |#

; projection on a subspace spanned by the variables in vars
(defn project (vars as)
    (cond ((nlistp as) as)
	  ((member (caar as) vars) 
	   (cons (car as) (project vars (cdr as))) )
	  (t (project vars (cdr as))) ) )

(lemma assoc-project (rewrite)
    (implies (member x vars)
	     (equal (assoc x (project vars as)) 
		    (assoc x as) ) )
    ((enable project)) )

(lemma project-putassoc (rewrite)
    (equal (project vars (putassoc key val as))
	   (if (member key vars) 
	       (putassoc key val (project vars as))
	     (project vars as) ) )
    ((enable project putassoc)) )

; all free variables belong to vs
(defn pure (flag vs exp)
    (if (equal flag 'list)
	(if (nlistp exp) nil
	  (and (pure t vs (car exp))
	       (pure 'list vs (cdr exp)) ) )
      (if (litatom exp) (member exp vs)
	(if (nlistp exp) t
	    (or (equal (car exp) 'quote)
		(pure 'list vs (cdr exp)) ) ) ) ) )

(lemma eval-project (rewrite)
    (implies (pure flag vars exp)
	     (equal (eval flag exp (project vars as))
		    (eval flag exp as) ) ) 
    ((enable assoc-project pure eval project)) )

(lemma project-append (rewrite)
    (equal (project vars (append x y))
	   (append (project vars x) (project vars y)) )
    ((enable project)) )

(defn intersection (x y)
  (if (nlistp x) x
    (if (member (car x) y) 
	(cons (car x) (intersection (cdr x) y))
      (intersection (cdr x) y) ) ) )

(lemma member-intersection (rewrite)
    (equal (member q (intersection x y))
	   (and (member q x) (member q y)) ) 
    ((enable intersection)) )

(lemma project-cleanalist (rewrite)
    (equal (project vars (cleanalist d as))
	   (cleanalist (intersection d vars) as) ) 
    ((enable project cleanalist intersection)) )

; project applied to all values in assoc-list
(defn map2project (vars as)
    (if (nlistp as) as
      (cons (cons (caar as) (project vars (cdar as)))
	    (map2project vars (cdr as)) ) ) )

(lemma lookup-map2project (rewrite)
    (equal (cdr (assoc q (map2project vars as)))
	   (project vars (cdr (assoc q as))) )
    ((enable map2project project lookup)) )

(defn subset (x y) 
    (if (nlistp x) t
        (and (member (car x) y) 
             (subset (cdr x) y) ) ) )

(lemma member-subset (rewrite)
    (implies (and (subset x y)
                  (member a x) )
             (member a y) ) 
    ((enable subset)) ) ; triv

(prove-lemma subset-extended (rewrite) ; auxiliary
    (implies (subset x y)
             (subset x (cons a y)) ) )

(prove-lemma subset-reflexive (rewrite)
    (subset x x) )

(lemma subset-append (rewrite)
    (equal (subset (append xs ys) zs) 
	   (and (subset xs zs)
		(subset ys zs) ) )
    ((enable subset)) )

(lemma cleanalist-project-subset (rewrite)
    (implies (subset d vars)
	     (equal (cleanalist d (project vars as))
		    (cleanalist d as) ) )
    ((enable project cleanalist subset)
     (do-not-generalize t) ) )

(lemma intersection-subset-right (rewrite)
    (subset (intersection d vars) vars) 
    ((enable intersection subset)) )

; projection applied to shared and private variables
(defn concproject (vars x)
    (cons (map2project vars (car x))
	  (project vars (cdr x)) ) )

(lemma concproject-shared (rewrite)
    (implies (member key vars)
	     (equal (lookup key (cdr (concproject vars x)))
		    (lookup key (cdr x)) ) )
    ((enable lookup concproject assoc-project)) )

(lemma concproject-private (rewrite)
    (implies (member key vars)
	     (equal (lookup key (privstate q (concproject vars x)))
		    (lookup key (privstate q  x)) ) )
    ((enable lookup concproject privstate lookup-map2project assoc-project)
     (do-not-induct t) ) )

(lemma eval-view-project (rewrite)
    (implies (and (pure t vars exp)
		  (member 'self vars) )
	     (equal (eval t exp 
			  (view (intersection d vars) q 
				(concproject vars x) ) )
		    (eval t exp (view d q x)) ) )
    ((use (eval-project (flag t) 
			(as (view d q x)) ))
     (enable project-append project-cleanalist lookup-map2project
	     shared privstate project concproject view
	     cleanalist-project-subset intersection-subset-right  )
     (do-not-induct t) ) )

; Remove from cmd all assignments to variables outside vars
(defn unghost0 (vars cmd)
    (cond ((nlistp cmd) cmd)
          ((nlistp (car cmd))
           (case (car cmd)
                 (put (if (member (cadr cmd) vars) cmd '(skip)))
                 (if (list 'if (cadr cmd) 
			   (unghost0 vars (caddr cmd))
                           (unghost0 vars (cadddr cmd)) ))
                 (otherwise cmd) ) )
          (t (cons (unghost0 vars (car cmd))
		   (unghost0 vars (cdr cmd)) )) ) )

; the variables in vars are not influenced by those outside
(defn pure-cmd (vars cmd)
    (cond ((nlistp cmd) t)
          ((nlistp (car cmd))
           (case (car cmd)
                 (put (implies (member (cadr cmd) vars)
			       (pure t vars (caddr cmd)) ))
                 (if (and (pure t vars (cadr cmd))
			  (pure-cmd vars (caddr cmd))
			  (pure-cmd vars (cadddr cmd)) ))
                 (otherwise t) ) )
          (t (and (pure-cmd vars (car cmd)) 
		  (pure-cmd vars (cdr cmd)) )) ) )

(lemma map2project-putassoc (rewrite)
    (implies (listp (assoc q as))
	     (equal (map2project vars 
    		       (putassoc q 
				 (putassoc key val (cdr (assoc q as))) 
				 as ) )
		    (if (member key vars)
			(putassoc q 
				 (putassoc key val 
 			             (cdr (assoc q (map2project vars as))) )
				 (map2project vars as) )
		      (map2project vars as)) ) )
    ((enable project-putassoc map2project putassoc project )) )

(lemma map2project-putassoc-inner (rewrite)
    (implies (member key vars)
	     (equal (map2project vars 
    		       (putassoc q 
				 (putassoc key val (cdr (assoc q as))) 
				 as ) )
		    (putassoc q 
				 (putassoc key val 
 			             (cdr (assoc q (map2project vars as))) )
				 (map2project vars as) ) ) )
    ((enable project-putassoc map2project putassoc project )) )

(defn occurs (q x)
    (listp (assoc q (car x))) )

(lemma concproject-putlocal (rewrite)
    (implies (occurs q x)
	     (equal (concproject vars (putlocal q key val x))
		    (if (member key vars)
			(putlocal q key val (concproject vars x))
		      (concproject vars x) ) ) )
    ((enable occurs concproject map2project-putassoc putlocal privstate)
     (do-not-induct t) ) )

(lemma concproject-putglobal (rewrite)
    (equal (concproject vars (putglobal q key val x))
	   (if (member key vars)
	       (putglobal q key val (concproject vars x))
	     (concproject vars x) ) )
    ((enable concproject putglobal project-putassoc)
     (do-not-induct t) ) )

(lemma occurs-preserved-putgen (rewrite)
    (implies (occurs q x) 
	     (occurs q (putgen d p key val x)) )
    ((enable occurs putgen putglobal putlocal putassoc assoc-put)) )

(lemma occurs-preserved-exe (rewrite)
    (implies (occurs q x) 
	     (occurs q (exe d p cmd x)) )
    ((enable occurs-preserved-putgen exe)) )

(lemma exe-project-unghost0 (rewrite)
    (implies (and (pure-cmd vars cmd)
		  (occurs q x)
		  (member 'self vars) )
	     (equal (concproject vars (exe d q cmd x))
		    (exe (intersection d vars) q
			 (unghost0 vars cmd)
			 (concproject vars x) ) ) )
    ((enable pure-cmd unghost0 exe member-intersection concproject-putglobal
	     occurs-preserved-exe pure putgen concproject-putlocal )
     (use (eval-view-project (exp (caddr cmd)))
	  (eval-view-project (exp (cadr cmd))) )
     (induct (exe d q cmd x)) (do-not-induct t) ) ) ; [ 0.0 1.6 0.1 ]

(defn touch (q as) (putassoc q (cdr (assoc q as)) as))
(defn ctouch (q x) (cons (touch q (car x)) (cdr x)))

(lemma touch-eq-eq (rewrite)
    (equal (equal (touch q x) x)
	   (listp (assoc q x)) )
    ((enable touch putassoc)) )

(lemma listp-assoc-touch (rewrite)
    (listp (assoc q (touch q x)))
    ((enable touch putassoc)) )

(lemma ctouch-occurs (rewrite)
    (occurs q (ctouch q x))
    ((enable ctouch occurs listp-assoc-touch)) )

(lemma map2project-touch (rewrite)
    (equal (map2project vars (touch q x))
	   (touch q (map2project vars x)) )
    ((enable touch map2project putassoc project )
     (do-not-generalize t) ) )

(lemma concproject-ctouch (rewrite)
    (equal (ctouch q (concproject vars x))
	   (concproject vars (ctouch q x)) )
    ((enable ctouch concproject map2project-touch)) )

(defn exec (d q cmd x)
    (exe d q cmd (ctouch q x)) )

(lemma exec-project-unghost0 (rewrite)
    (implies (and (pure-cmd vars cmd)
		  (member 'self vars) )
	     (equal (concproject vars (exec d q cmd x))
		    (exec (intersection d vars) q
			  (unghost0 vars cmd)
			  (concproject vars x) ) ) )
    ((enable concproject-ctouch exe-project-unghost0 ctouch-occurs exec)
     (do-not-induct t) ) ) 

(defn cleanup (cmd)
    (cond ((nlistp cmd) '(skip))
          ((nlistp (car cmd))
           (if (equal (car cmd) 'if)
               (let ((cm0 (cleanup (caddr cmd)))
                     (cm1 (cleanup (cadddr cmd))) )
                    (if (equal cm1 '(skip))
                        (list 'if (cadr cmd) cm0)
                        (list 'if (cadr cmd) cm0 cm1) ) )
               cmd ) )
          (t (let ((cm0 (cleanup (car cmd)))
                   (cm1 (cleanup (cdr cmd))) )
                  (cond ((equal cm0 '(skip)) cm1)
                        ((equal cm1 '(skip)) cm0)
                        ((nlistp (car cm1))
                         (list cm0 cm1))
                        (t (cons cm0 cm1)) ) )) ) )

(lemma exe-cleanup (rewrite)
    (equal (exe d p (cleanup cmd) x) 
           (exe d p cmd x) )
    ((enable exe cleanup)) ) ; [ 0.0 0.1 0.1 ]

(lemma exec-cleanup (rewrite)
    (equal (exec d p (cleanup cmd) x) 
           (exec d p cmd x) )
    ((enable exec exe-cleanup)) ) ; [ 0.0 0.1 0.1 ]

(defn unghost (vars cmd)
    (cleanup (unghost0 vars cmd)) )

(lemma exec-project-unghost (rewrite)
    (implies (and (pure-cmd vars cmd)
		  (member 'self vars) )
	     (equal (concproject vars (exec d q cmd x)) 
		    (exec (intersection d vars) q
			  (unghost vars cmd)
			  (concproject vars x) ) ) )
    ((enable exec-project-unghost0 unghost exec-cleanup)
     (do-not-induct t) ) ) 

(defn unghost-pc (vars cmd)
    (if (nlistp cmd) cmd
      (cons (if (car cmd)
		(cons (caar cmd) 
		      (let ((rhs (unghost vars (cdar cmd))))
			(if (member (car rhs) '(put if))
			    (list rhs)
			  rhs ) ) )
	      f )
	    (unghost-pc vars (cdr cmd)) ) ) )

(lemma unghost-pc-unghost (rewrite)
    (equal (cdr (assoc pc (unghost-pc vars cmd)))
	   (if (assoc pc cmd)
	       (let ((res (unghost vars (cdr (assoc pc cmd)))))
		 (if (member (car res) '(put if))
		     (list res)
		   res ) )
	     0 ) )
    ((enable unghost-pc unghost cleanup)) )

(defn pure-cmd-pc (vars cmd)
    (if (nlistp cmd) t
      (and (listp (car cmd))
	   (pure-cmd vars (cdar cmd))
	   (pure-cmd-pc vars (cdr cmd)) ) ) )

(lemma pure-cmd-pc-implies (rewrite)
    (implies (pure-cmd-pc vars cmd)
	     (pure-cmd vars (cdr (assoc pc cmd))) )
    ((enable pure-cmd pure-cmd-pc)) )

(lemma pc-concproject (rewrite)
    (implies (member 'pc vars)
	     (equal (pc q (concproject vars x))
		    (pc q x) ) )
    ((enable pc concproject-private)) )

(lemma putlocal-concproject (rewrite)
    (implies (member key vars) 
	     (equal (putlocal q key val (concproject vars x))
		    (concproject vars (putlocal q key val x)) ) )
    ((enable putlocal concproject privstate occurs 
	     map2project-putassoc-inner)
     (do-not-induct t) ) )

(lemma putlocal-occurs (rewrite)
    (occurs q (putlocal q key val x)) 
    ((enable occurs putlocal assoc-put)) )

(lemma exepc-project-unghost (rewrite)
    (implies (and (pure-cmd-pc vars cmd)
		  (member 'self vars)
		  (member 'pc vars) )
	     (equal (concproject vars (exepc d q cmd x)) 
		    (exepc (intersection d vars) q
			   (unghost-pc vars cmd)
			   (concproject vars x) ) ) )
    ((enable exe-project-unghost0 putlocal-concproject exepc unghost0
	     putlocal-occurs pc-concproject pure-cmd-pc-implies exe
	     unghost-pc unghost unghost-pc-unghost exe-cleanup )
     (do-not-induct t) ) )

#| This theory can be instantiated with apply = apply$, eval = eval$. |#

(defn exe$ (d q cmd x)
    (cond ((nlistp cmd) x)
          ((nlistp (car cmd))
           (case (car cmd)
                 (put (putgen d q (cadr cmd) 
                              (eval$ t (caddr cmd) (view d q x))
                              x ))
                 (if (if (eval$ t (cadr cmd) (view d q x))
                         (exe$ d q (caddr cmd) x)
                         (exe$ d q (cadddr cmd) x) ))
                 (otherwise x) ) )
          (t (exe$ d q (cdr cmd) 
                  (exe$ d q (car cmd) x) )) ) )

(defn exepc$ (d q cmd x)
    (exe$ d q (cdr (assoc (pc q x) cmd))
	  (putlocal q 'pc (add1 (pc q x)) x) ) )

(functionally-instantiate private-vars-exepc$ (rewrite)
    (implies (not (equal p q)) 
             (equal (privstate q (exepc$ d p cmd x))
                    (privstate q x) ) ) 
    private-vars-exepc 
    ((exe exe$) (eval eval$) (apply apply$) (exepc exepc$)) )

(functionally-instantiate exepc$-project-unghost (rewrite)
    (implies (and (pure-cmd-pc vars cmd)
		  (member 'self vars)
		  (member 'pc vars) )
	     (equal (concproject vars (exepc$ d q cmd x)) 
		    (exepc$ (intersection d vars) q
			   (unghost-pc vars cmd)
			   (concproject vars x) ) ) )
    exepc-project-unghost
    ((exe exe$) (eval eval$) (apply apply$) (exepc exepc$)) )

#| Auxiliary functions |#

(defn myor (a b) (if a a b) )

; if a command is not pure, a witness is found by 
(defn unpure-cmd (vars cmd)
    (cond ((nlistp cmd) f)
          ((nlistp (car cmd))
           (case (car cmd)
                 (put (if (not (member (cadr cmd) vars)) f
			(if (pure t vars (caddr cmd)) f
			  (list cmd) ) ))
                 (if (if (pure t vars (cadr cmd))
			 (myor (unpure-cmd vars (caddr cmd))
			     (unpure-cmd vars (cadddr cmd)) )
		       (cons 'if (list (cadr cmd))) ))
                 (otherwise f) ) )
          (t (myor (unpure-cmd vars (car cmd)) 
		 (unpure-cmd vars (cdr cmd)) )) ) )

(lemma unpure-cmd-not-pure (rewrite)
    (equal (not (unpure-cmd vars cmd))
	   (pure-cmd vars cmd) )
    ((enable myor unpure-cmd pure-cmd pure)) )

; if a pc-command is not pure, a witness is found by 
(defn unpure-cmd-pc (vars cmd)
    (if (nlistp cmd) f
      (if (nlistp (car cmd)) (cons f (car cmd))
	(if (pure-cmd vars (cdar cmd))
	    (unpure-cmd-pc vars (cdr cmd))
	  (cons (caar cmd) (unpure-cmd vars (cdar cmd))) ) ) ) )

(lemma unpure-cmd-pc-not-pure (rewrite)
    (equal (pure-cmd-pc vars cmd)
	   (not (unpure-cmd-pc vars cmd)) ) 
    ((enable unpure-cmd-pc pure-cmd-pc)) )

; a list of the function symbols occurring in an expression
(defn occ-funs (flag exp)
    (cond ((equal flag 'list) 
	   (if (nlistp exp) nil
	     (union (occ-funs t (car exp))
		    (occ-funs 'list (cdr exp)) ) ) )
	  ((nlistp exp) nil)
	  ((equal (car exp) 'quote) nil)
	  (t (add-to-set (car exp) (occ-funs 'list (cdr exp)))) ) )

; a list of the function symbols occurring in a command
(defn occ-funs-cmd (cmd)
    (cond ((nlistp cmd) nil)
	  ((nlistp (car cmd))
	   (case (car cmd)
		 (put (occ-funs t (caddr cmd)))
		 (if (union (occ-funs t (cadr cmd))
			    (union (occ-funs-cmd (caddr cmd))
				   (occ-funs-cmd (cadddr cmd)) ) ))
		 (otherwise nil) ) )
	  (t (union (occ-funs-cmd (car cmd))
		    (occ-funs-cmd (cdr cmd)) )) ) )

; a list of the function symbols occurring in a pc-command
(defn occ-funs-cmd-pc (cmd)
    (if (nlistp cmd) nil
      (union (occ-funs-cmd (cdar cmd))
	     (occ-funs-cmd-pc (cdr cmd)) ) ) )

(deftheory project-th 
    (unghost0 unghost unghost-pc pure pure-cmd pure-cmd-pc cleanup
	      *1*unghost0 *1*unghost *1*unghost-pc *1*pure *1*pure-cmd 
	      *1*pure-cmd-pc *1*cleanup) )

; Analysis of the list of participating processes 

(defn madd-to-set (a xs) ; addition at the end, if needed
    (cond ((nlistp xs) (cons a xs))
	  ((equal a (car xs)) xs)
	  (t (cons (car xs) (madd-to-set a (cdr xs)))) ) )

(lemma madd-to-set-member-equal (rewrite)
    (implies (member a xs)
	     (equal (madd-to-set a xs) xs) )
    ((enable madd-to-set)) )

(lemma member-madd-to-set (rewrite)
    (equal (member a (madd-to-set b xs))
	   (or (equal a b)
	       (member a xs) ) )
    ((enable madd-to-set)) )

(lemma strip-cars-putassoc (rewrite)
    (equal (strip-cars (putassoc key val as))
	   (madd-to-set key (strip-cars as)) )
    ((enable putassoc madd-to-set)) )

(defn processes (x)
    (strip-cars (car x)) )

(lemma lookup-outside (rewrite)
    (implies (assoc q as)
	     (member q (strip-cars as)) ) )

(lemma privstate-outside (rewrite)
    (implies (not (member q (processes x)))
	     (equal (privstate q x) 0) )
    ((enable lookup-outside processes privstate)
     (use (lookup-outside (as (car x)))) ) )

(lemma processes-putlocal (rewrite)
    (equal (processes (putlocal q var w x))
	   (madd-to-set q (processes x)) )
    ((enable processes putlocal strip-cars-putassoc)) )

(lemma processes-putglobal (rewrite)
    (implies (member q (processes x))
	     (equal (processes (putglobal q var w x))
		    (processes x) ) )
    ((enable processes putglobal)
     (do-not-induct t) ) )

(lemma processes-putgen (rewrite)
    (implies (member q (processes x))
	     (equal (processes (putgen d q var w x))
		    (processes x) ) )
    ((enable putgen processes-putglobal processes-putlocal 
	     madd-to-set-member-equal )
     (do-not-induct t) ) )

(lemma processes-exe (rewrite)
    (implies (member q (processes x))
	     (equal (processes (exe d q cmd x))
		    (processes x) ) )
    ((enable exe processes-putgen)) )

(lemma processes-exepc (rewrite)
    (equal (processes (exepc d q cmd x))
	   (madd-to-set q (processes x)) )
    ((enable exepc processes-putlocal processes-exe member-madd-to-set 
	     madd-to-set-member-equal )) )

; Towards relational specifications

(defn lor (xs)
    (If (nlistp xs) f
      (if (car xs) t
	(lor (cdr xs)) ) ) )

(defn land (xs)
    (if (nlistp xs) t
      (if (car xs) (land (cdr xs))
	f ) ) )

; equality of assoc-lists xs and ys with respect to the elements of lis 
(defn eqlis-lookup (lis xs ys)
    (if (nlistp lis) t
      (and (equal (lookup (car lis) xs)
		  (lookup (car lis) ys) )
	   (eqlis-lookup (cdr lis) xs ys) ) ) )

(lemma lookup-outside-subdomain (rewrite)
    (implies (and (subset (strip-cars db) os)
		  (not (member ob os)) )
	     (equal (lookup ob db) 0) )
    ((enable subset lookup)) )

(lemma lookup-inside-subdomain (rewrite)
    (implies (and (member ob os)
		  (eqlis-lookup os db0 db1) )
	     (equal (lookup ob db0) (lookup ob db1)) )
    ((enable eqlis-lookup lookup)) )

(lemma lookup-eqlis-lookup (rewrite)
    (implies (and (eqlis-lookup os db0 db1)
		  (subset (strip-cars db0) os)
		  (subset (strip-cars db1) os) )
	     (equal (lookup ob db0) (lookup ob db1)) )
    ((enable lookup-outside-subdomain)
     (use (lookup-inside-subdomain))
     (do-not-induct t) ) )

; The function eqlis-lookup-lis is an equivalence relation:

(lemma eqlis-lookup-reflexive (rewrite)
    (eqlis-lookup lis xs xs)
    ((enable eqlis-lookup)) )

(lemma eqlis-lookup-symmetric (rewrite)
    (implies (eqlis-lookup lis xs ys) (eqlis-lookup lis ys xs))
    ((enable eqlis-lookup)) )

(lemma eqlis-lookup-transitive (rewrite)
    (implies (and (eqlis-lookup lis xs ys) (eqlis-lookup lis ys zs))
	     (eqlis-lookup lis xs zs) )
    ((enable eqlis-lookup)) )

(lemma subset-append-left (rewrite)
    (subset xs (append xs ys)) 
    ((enable subset)) )

(lemma subset-append-right (rewrite)
    (subset ys (append xs ys)) 
    ((enable subset)) )

#| We now define eq-lookup, which expresses equality of the 
assoc-lists xs and ys regarded as functions. |#

(defn eq-lookup (xs ys)
    (eqlis-lookup (append (strip-cars xs) (strip-cars ys)) xs ys) )

(lemma eq-lookup-all (rewrite)
    (implies (eq-lookup xs ys)
	     (equal (lookup a xs) (lookup a ys)) ) 
    ((enable eq-lookup subset-append-left subset-append-right
	     lookup-eqlis-lookup )) )

(lemma eq-lookup-eqlis-lookup (rewrite)
    (implies (eq-lookup xs ys)
	     (eqlis-lookup lis xs ys) )
    ((enable eq-lookup-all eqlis-lookup)) )

(lemma eq-lookup-reflexive (rewrite)
    (eq-lookup xs xs)
    ((enable eqlis-lookup-reflexive eq-lookup)) )

(lemma eq-lookup-symmetric (rewrite)
    (implies (eq-lookup xs ys) 
	     (eq-lookup ys xs) )
    ((enable eq-lookup-eqlis-lookup eqlis-lookup-symmetric)
     (expand (eq-lookup ys xs)) ) )

(lemma eq-lookup-transitive (rewrite)
    (implies (and (eq-lookup xs ys) 
		  (eq-lookup ys zs) )
	     (eq-lookup xs zs) )
    ((enable eq-lookup-eqlis-lookup) (do-not-induct t)
     (use (eqlis-lookup-transitive 
	   (lis (append (strip-cars xs) (strip-cars zs))) ))
     (expand (eq-lookup xs zs)) ) )

#| Function eval2$ serves to evaluate relational specifications.
If we need axiomatically introduced function symbols, function apply$
must be strengthened to evaluate them. |# 
(defn eval2$ (flag x as bs) 
    (if (equal flag 'list)
	(if (nlistp x) nil
	  (cons (eval2$ t (car x) as bs)
		(eval2$ 'list (cdr x) as bs) ) )
      (cond ((litatom x) (cdr (assoc x as)))
            ((nlistp x) x)
	    (t (case (car x) 
		     (quote (cadr x))
		     (new (eval2$ t (cadr x) bs as)) 
		     (or (lor (eval2$ 'list (cdr x) as bs))) 
		     (and (land (eval2$ 'list (cdr x) as bs))) 
		     (diag (eqlis-lookup (cdr x) as bs))
		     (otherwise 
		      (apply$ (car x) 
			      (eval2$ 'list (cdr x) as bs) ) ) )) ) ) )

; The standard application is by means of 
(defn interpret$ (d spec q x y)
    (eval2$ t spec (view d q x) (view d q y)) )

#| Possibly with view replaced by sview. Indeed, occasionally, 
processes can be allowed to inspect the entire global state via 
'global-state. This would be overridden by a shared variable with 
the same name. We use this here only for specification purposes. |# 

(defn sview (d q x) ; part of the state visible to process q
   (append (shared d x) 
	   (list* (cons 'self q)
		  (cons 'global-state x)
		  (privstate q x)) ) )

(make-lib "newprelude")