← Back to branch summary

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

« back to all changes in this revision

Viewing changes to books/centaur/bitops/ihsext-basics.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/centaur/bitops/ihsext-basics.lisp
40
40
 
41
41
(include-book "centaur/misc/arith-equivs" :dir :system)
42
42
(include-book "xdoc/top" :dir :system)
43
 
(include-book "tools/defredundant" :dir :system)
44
43
 
45
44
(local (in-theory (enable* arith-equiv-forwarding)))
46
45
(local (include-book "ihs/quotient-remainder-lemmas" :dir :system))
55
54
  :long "<p>BOZO this needs a lot of documentation.  For now you're best
56
55
off looking at the source code.</p>")
57
56
 
58
 
(defredundant-events
 
57
 
 
58
;; [Jared] this was causing errors, I think due to the doc-string stripping code
 
59
;; not working when :doc nil is given.  Switching it to use std/util/defredundant
 
60
;; instead.
 
61
;; (include-book "tools/defredundant" :dir :system)
 
62
;; (defredundant-events
 
63
 
 
64
(encapsulate
 
65
  ()
 
66
  (local (include-book "std/util/defredundant" :dir :system))
 
67
  (make-event
 
68
   (b* ((imports '(
 
69
 
59
70
; There are too many rules with forced hyps in logops-lemmas.  We'll locally
60
71
; include it and redundantly define many of the useful theorems.
61
72
 
62
 
  constant-syntaxp
63
 
  ash-0
64
 
  cancel-equal-lognot
65
 
  commutativity-of-logand
66
 
  simplify-logand
67
 
  commutativity-of-logior
68
 
  simplify-logior
69
 
  commutativity-of-logxor
70
 
  simplify-logxor
71
 
  simplify-bit-functions
72
 
  unsigned-byte-p-base-case
73
 
  unsigned-byte-p-0
74
 
  unsigned-byte-p-plus
75
 
  difference-unsigned-byte-p
76
 
  ;; signed-byte-p-base-cases
77
 
  ;; backchain-signed-byte-p-to-unsigned-byte-p
78
 
  loghead-identity
79
 
  ;; loghead-0-i remove hyp
80
 
  ;; loghead-size-0 remove hyp
81
 
  ;; loghead-leq remove force
82
 
  bitp-loghead-1
83
 
  logtail-identity
84
 
  ;; logtail-logtail remove hyps
85
 
  ;; logtail-0-i remove hyp
86
 
  ;; logtail-size-0 remove hyp
87
 
  ;; logtail-leq remove hyp
88
 
  ;; logtail-unsigned-byte-p remove hyp
89
 
  ;; logtail-loghead remove hyp
90
 
  ;; associativity-of-logapp remove hyp
91
 
 
92
 
  logext-identity
93
 
 
94
 
  ;; we'll prove a stronger rewrite rule and disable this
95
 
  ;; rw, but it's a good elim
96
 
  logcar-logcdr-elim
97
 
 
98
 
  ;; these are weird but won't hurt much
99
 
  logcar-2*i
100
 
  logcar-i+2*j
101
 
  logcdr-2*i
102
 
  logcdr-i+2*j
103
 
 
104
 
  ;; logbitp-0-minus-1 remove hyps
105
 
  ;; logbit-0-minus-1 remove hyps
106
 
 
107
 
  signed-byte-p-logops)
 
73
                   constant-syntaxp
 
74
                   ash-0
 
75
                   cancel-equal-lognot
 
76
                   commutativity-of-logand
 
77
                   simplify-logand
 
78
                   commutativity-of-logior
 
79
                   simplify-logior
 
80
                   commutativity-of-logxor
 
81
                   simplify-logxor
 
82
                   simplify-bit-functions
 
83
                   unsigned-byte-p-base-case
 
84
                   unsigned-byte-p-0
 
85
                   unsigned-byte-p-plus
 
86
                   difference-unsigned-byte-p
 
87
                   ;; signed-byte-p-base-cases
 
88
                   ;; backchain-signed-byte-p-to-unsigned-byte-p
 
89
                   loghead-identity
 
90
                   ;; loghead-0-i remove hyp
 
91
                   ;; loghead-size-0 remove hyp
 
92
                   ;; loghead-leq remove force
 
93
                   bitp-loghead-1
 
94
                   logtail-identity
 
95
                   ;; logtail-logtail remove hyps
 
96
                   ;; logtail-0-i remove hyp
 
97
                   ;; logtail-size-0 remove hyp
 
98
                   ;; logtail-leq remove hyp
 
99
                   ;; logtail-unsigned-byte-p remove hyp
 
100
                   ;; logtail-loghead remove hyp
 
101
                   ;; associativity-of-logapp remove hyp
 
102
 
 
103
                   logext-identity
 
104
 
 
105
                   ;; we'll prove a stronger rewrite rule and disable this
 
106
                   ;; rw, but it's a good elim
 
107
                   logcar-logcdr-elim
 
108
 
 
109
                   ;; these are weird but won't hurt much
 
110
                   logcar-2*i
 
111
                   logcar-i+2*j
 
112
                   logcdr-2*i
 
113
                   logcdr-i+2*j
 
114
 
 
115
                   ;; logbitp-0-minus-1 remove hyps
 
116
                   ;; logbit-0-minus-1 remove hyps
 
117
 
 
118
                   signed-byte-p-logops))
 
119
        (events (std::defredundant-fn imports nil state)))
 
120
     (acl2::value events))))
108
121
 
109
122
(defconst *ihs-extensions-disables*
110
123
  '(floor mod expt ash evenp oddp
2474
2487
    :hints (("goal" :in-theory (e/d* (ihsext-recursive-redefs
2475
2488
                                      ihsext-inductions)
2476
2489
                                     (logcdr-<-const
2477
 
                                      mod-x-y-=-x+y))
 
2490
                                      mod-x-y-=-x+y-for-rationals))
2478
2491
             :induct (and (logsquash m x)
2479
2492
                          (logsquash n x))
2480
2493
             :expand ((:free (b) (logsquash n b))
2488
2501
    :hints (("goal" :in-theory (e/d* (ihsext-recursive-redefs
2489
2502
                                      ihsext-inductions)
2490
2503
                                     (logcdr-<-const
2491
 
                                      MOD-X-Y-=-X+Y))
 
2504
                                      MOD-X-Y-=-X+Y-for-rationals))
2492
2505
             :induct (and (logsquash m x)
2493
2506
                          (logsquash n x))
2494
2507
             :expand ((:free (b) (logsquash n b))
2936
2949
             :in-theory (disable signed-byte-p
2937
2950
                                 minus-to-lognot))))
2938
2951
 
 
2952
  (defthm logapp-sign
 
2953
    (equal (< (logapp size i j) 0)
 
2954
           (< (ifix j) 0))
 
2955
    :hints (("goal" :induct (logapp size i j)
 
2956
             :in-theory (disable (force)))))
 
2957
 
2939
2958
  (add-to-ruleset ihsext-basic-thms '(unsigned-byte-p-of-logapp
2940
 
                                      signed-byte-p-of-logapp))
 
2959
                                      signed-byte-p-of-logapp
 
2960
                                      logapp-sign))
2941
2961
 
2942
2962
  ;; (defthm logapp-zeros
2943
2963
  ;;   (equal (logapp i 0 0) 0))
3143
3163
                                     logmaskp*
3144
3164
                                     ihsext-recursive-redefs)
3145
3165
                                    ((force)))))
3146
 
    :rule-classes ((:definition :clique (bitmaskp)
3147
 
                    :controller-alist ((bitmaskp t)))))
 
3166
    :rule-classes ((:definition :clique (bitmaskp$inline)
 
3167
                    :controller-alist ((bitmaskp$inline t)))))
3148
3168
 
3149
3169
  (local (in-theory (disable bitmaskp)))
3150
3170
 
3332
3352
  (local (in-theory (enable* arith-equiv-forwarding)))
3333
3353
  (local (in-theory (enable logrev1 logrev)))
3334
3354
 
3335
 
  (in-theory (disable (:type-prescription logrev))) ;; Too weak (integerp)
 
3355
  (in-theory (disable (:t logrev))) ;; Too weak (integerp)
3336
3356
 
3337
3357
  (defthm logrev-type
3338
3358
    ;; Redundant with ihs/basic-definitions.lisp
3339
 
    (natp (logrev size i))
 
3359
    (b* ((nat (logrev$inline size i)))
 
3360
      (natp nat))
3340
3361
    :rule-classes :type-prescription)
3341
3362
 
3342
3363
  (local (defthm natp-of-logrev1
3410
3431
                 (logior (logrev size (logcdr i))
3411
3432
                         (ash (logcar i) size)))))
3412
3433
      :rule-classes ((:definition
3413
 
                      :clique (logrev)
3414
 
                      :controller-alist ((logrev t nil))))))
 
3434
                      :clique (logrev$inline)
 
3435
                      :controller-alist ((logrev$inline t nil))))))
3415
3436
 
3416
3437
  (add-to-ruleset ihsext-recursive-redefs '(logrev**))
3417
3438
  (add-to-ruleset ihsext-redefs '(logrev**))
3419
3440
  (defthmd logrev-induct
3420
3441
    t
3421
3442
    :rule-classes ((:induction
3422
 
                    :pattern (logrev size i)
 
3443
                    :pattern (logrev$inline size i)
3423
3444
                    :scheme (logbitp-ind size i))))
3424
3445
 
3425
3446
  (add-to-ruleset ihsext-inductions '(logrev-induct))