← Back to branch summary

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

« back to all changes in this revision

Viewing changes to books/workshops/2006/pike-shields-matthews/core_verifier/books/ihs-defthms-help.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/2006/pike-shields-matthews/core_verifier/books/ihs-defthms-help.lisp
 
1
#|
 
2
  Book:    ihs-defthms-help
 
3
  Copyright: (c) 2005 Galois Connections, Inc.
 
4
  Author:    Lee Pike, Galois Connections, Inc. <leepike@galois.com>
 
5
|#
 
6
 
 
7
 
 
8
(in-package "ACL2")
 
9
 
 
10
(include-book "source_shallow")
 
11
 
 
12
; Edited by Matt K.:
 
13
; (include-book "super-ihs" :dir :super-ihs)
 
14
(include-book "coi/super-ihs/super-ihs" :dir :system)
 
15
 
 
16
 
 
17
(defun log-rep-hlp (x i)
 
18
  (let ((val (if (logbitp i x) T NIL)))
 
19
  (if (zp i) (list val)
 
20
    (cons val (log-rep-hlp x (- i 1))))))
 
21
 
 
22
;; Lil' endian representation of x.  
 
23
(defun log-rep (x)
 
24
  (let ((size (nbits x)))
 
25
    (if (zp size) (list NIL)
 
26
      (reverse (log-rep-hlp x (- size 1))))))
 
27
 
 
28
(defun nat-rep-hlp (bin-list i)
 
29
  (if (endp bin-list) 0
 
30
    (let ((val (if (nth i bin-list) 1 0)))
 
31
      (if (zp i) val
 
32
        (+ (* val
 
33
              (expt2 i))
 
34
           (nat-rep-hlp bin-list (- i 1)))))))
 
35
 
 
36
(defun nat-rep (bin-lst)
 
37
  (nat-rep-hlp bin-lst (- (len bin-lst) 1)))
 
38
 
 
39
;; Helper needed by iterators yielding bits
 
40
(defun c-update-bit (i b w)
 
41
  (let ((hi-bits (logtail (+ i 1) w)))
 
42
    (logapp i w (logapp 1 b hi-bits))))
 
43
 
 
44
 
 
45
  (defthmd loghead-0 (equal (loghead 0 i) 0))
 
46
 
 
47
  (defthm c-word--thm
 
48
    (implies (and (natp i)
 
49
                  (natp k)
 
50
                  (natp n)
 
51
                  (natp m)
 
52
                  (<= n m))
 
53
             (equal (loghead n (c-word-- m i k))
 
54
                    (loghead n (- i k))))
 
55
    :hints (("Goal" :in-theory (enable c-word--))))
 
56
 
 
57
  (defthm nat-rep-loghead-1
 
58
    (implies (natp i)
 
59
             (equal (nat-rep 
 
60
                     (reverse 
 
61
                      (list 
 
62
                       (equal (loghead 1 i) 1))))
 
63
                    (loghead 1 i))))
 
64
 
 
65
(defthm less-loghead-expt 
 
66
  (< (loghead j i) (expt2 j)) 
 
67
  :hints (("Goal" :in-theory (enable loghead-when-i-is-not-an-integerp))))
 
68