← Back to branch summary

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

« back to all changes in this revision

Viewing changes to books/cgen/rem-and-floor.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/cgen/rem-and-floor.lisp
1
 
#|$ACL2s-Preamble$;
2
 
(ld ;; Newline to fool ACL2/cert.pl dependency scanner
3
 
 "portcullis.lsp")
4
 
(acl2::begin-book);$ACL2s-Preamble$|#
5
 
 
6
 
 
7
 
(in-package "DEFDATA")
8
 
 
9
 
(encapsulate nil
10
 
  
11
 
  ;; load in & build up some theory on integer division
12
 
  
13
 
  (local (include-book "arithmetic-5/top" :dir :system))
14
 
  
15
 
  (defthm floor-less
16
 
    (implies (and (integerp x)
17
 
                  (< 0 x)
18
 
                  (integerp y)
19
 
                  (<= 2 y))
20
 
             (< (floor x y) x))
21
 
    :rule-classes (:linear :rewrite))
22
 
  
23
 
  (defthm floor-0
24
 
    (implies (equal x 0)
25
 
             (equal (floor x y) x)))
26
 
  
27
 
  (defthm floor-less-eq
28
 
    (implies (and (integerp x)
29
 
                  (<= 0 x)
30
 
                  (integerp y)
31
 
                  (<= 2 y))
32
 
             (<= (floor x y) x))
33
 
    :hints (("Goal" :in-theory (disable floor)
34
 
                    :cases ((< 0 x))))
35
 
    :rule-classes (:linear :rewrite))
36
 
 
37
 
  (defthm rem-floor-decomp
38
 
    (implies (and (integerp x)
39
 
                  (<= 0 x)
40
 
                  (integerp y)
41
 
                  (<= 0 y))
42
 
             (equal (+ (rem x y)
43
 
                       (* y
44
 
                          (floor x y)))
45
 
                    x)))
46
 
  
47
 
  (defthm rem-0
48
 
    (equal (rem 0 x)
49
 
           0))
50
 
  
51
 
  (defthm rem--0
52
 
    (implies (acl2-numberp x)
53
 
             (equal (rem x 0)
54
 
                    x)))
55
 
  
56
 
  (defthm rem-integerp
57
 
    (implies (and (integerp x)
58
 
                  (integerp y))
59
 
             (integerp (rem x y)))
60
 
    :rule-classes (:rewrite :type-prescription))
61
 
  
62
 
  (defthm rem-upper-bound
63
 
    (implies (and (integerp x) (<= 0 x)
64
 
                  (integerp y) (< 0 y))
65
 
             (<= (rem x y) x))
66
 
    :rule-classes (:linear :rewrite))
67
 
 
68
 
  (local (in-theory (disable rem)))
69
 
  
70
 
  (defthm rem-lower-bound2
71
 
    (implies (and (integerp x) (<= 0 x) (integerp y) (<= 0 y))
72
 
             (<= 0 (rem x y)))
73
 
    :rule-classes (:linear :rewrite)
74
 
    :hints (("Goal" :cases ((equal x 0)
75
 
                            (equal y 0)))))
76
 
  
77
 
  (defthm rem-upper-bound2
78
 
    (implies (and (integerp x) (<= 0 x) (integerp y) (< 0 y))
79
 
             (< (rem x y) y))
80
 
    :rule-classes (:linear :rewrite)
81
 
    :hints (("Goal" :cases ((equal x 0)))))
82
 
  
83
 
  (defthm floor-integerp
84
 
    (implies (and (integerp x)
85
 
                  (integerp y))
86
 
             (integerp (floor x y)))
87
 
    :rule-classes (:rewrite :type-prescription))
88
 
  
89
 
  (defthm floor-nat
90
 
    (implies (and (integerp x)
91
 
                  (<= 0 x)
92
 
                  (integerp y)
93
 
                  (<= 0 y))
94
 
             (<= 0 (floor x y)))
95
 
    :rule-classes (:linear :rewrite)))
96
 
 
97
 
(in-theory (disable rem floor))#|ACL2s-ToDo-Line|#
98