← Back to branch summary

~ubuntu-branches/ubuntu/wily/acl2/wily

« back to all changes in this revision

Viewing changes to books/workshops/2000/manolios/pipeline/pipeline/top/alist-thms.lisp

  • Committer: Package Import Robot
  • Author(s): Camm Maguire
  • Date: 2015-01-16 10:35:45 UTC
  • mfrom: (3.3.26 sid)
  • Revision ID: package-import@ubuntu.com-20150116103545-prehe9thgo79o8w8
Tags: 7.0-1
New upstream release

Show diffs side-by-side

added added

removed removed

Lines of Context:
books/workshops/2000/manolios/pipeline/pipeline/top/alist-thms.lisp
 
1
;  Copyright (C) 2000 Panagiotis Manolios
 
2
 
 
3
;  This program is free software; you can redistribute it and/or modify
 
4
;  it under the terms of the GNU General Public License as published by
 
5
;  the Free Software Foundation; either version 2 of the License, or
 
6
;  (at your option) any later version.
 
7
 
 
8
;  This program is distributed in the hope that it will be useful,
 
9
;  but WITHOUT ANY WARRANTY; without even the implied warranty of
 
10
;  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 
11
;  GNU General Public License for more details.
 
12
 
 
13
;  You should have received a copy of the GNU General Public License
 
14
;  along with this program; if not, write to the Free Software
 
15
;  Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139, USA.
 
16
 
 
17
;  Written by Panagiotis Manolios who can be reached as follows.
 
18
 
 
19
;  Email: pete@cs.utexas.edu
 
20
 
 
21
;  Postal Mail:
 
22
;  Department of Computer Science
 
23
;  The University of Texas at Austin
 
24
;  Austin, TX 78701 USA
 
25
 
 
26
(in-package "ACL2")
 
27
 
 
28
(defun make-sym (s suf)
 
29
; Returns the symbol s-suf.
 
30
  (declare (xargs :guard (and (symbolp s) (symbolp suf))))
 
31
  (intern-in-package-of-symbol
 
32
   (concatenate 'string
 
33
                (symbol-name s) 
 
34
                "-"
 
35
                (symbol-name suf))
 
36
   s))
 
37
 
 
38
(defmacro defung (&rest def) 
 
39
; A function definition that has a declare followed by a list of the
 
40
; form ((thm) commands), where commands can be anything that you would
 
41
; give to a defthm (look at defthm documentation), specifically it is:
 
42
;        :rule-classes rule-classes
 
43
;        :instructions instructions
 
44
;        :hints        hints
 
45
;        :otf-flg      otf-flg
 
46
;        :doc          doc-string
 
47
;
 
48
; The if test checks for documentation strings.  
 
49
  (list 'progn
 
50
        (cons 'defun (append (list (first def)
 
51
                                   (second def)
 
52
                                   (third def))
 
53
                             (if (stringp (third def))
 
54
                                 (list (fourth def) 
 
55
                                       (sixth def))
 
56
                               (list (fifth def)))))
 
57
        (append (list 'defthm (make-sym (car def) 'return-type))
 
58
                (if (stringp (third def))
 
59
                    (fifth def)
 
60
                  (fourth def)))))
 
61
 
 
62
(defung update-valuation (v s val)
 
63
"gives val[v <- s] if v is in val, otherwise gives val U [v <- s]"
 
64
  (declare (xargs :guard (alistp val))) 
 
65
  ((implies (alistp val) (alistp (update-valuation v s val))))
 
66
  (if (endp val)
 
67
      (list (cons v s))
 
68
    (if (equal v (caar val))
 
69
        (acons v s (cdr val))
 
70
      (cons (car val) (update-valuation v s (cdr val))))))
 
71
 
 
72
(defun value-of (x alist)
 
73
  (declare (xargs :guard (alistp alist))) 
 
74
  (cdr (assoc-equal x alist)))
 
75
 
 
76
(defthm update-val
 
77
  (equal (value-of n (update-valuation m z x))
 
78
         (if (equal n m)
 
79
             z
 
80
           (value-of n x))))
 
81
 
 
82
(defthm update-valuation-update-valuation-same
 
83
  (equal (update-valuation i v1 (update-valuation i v2 l))
 
84
         (update-valuation i v1 l)))
 
85