[axe] Organize some supporting rules.

Author: ericwhitmansmith

books/kestrel/axe/arithmetic-rules-axe.lisp

@@ -10,6 +10,8 @@
 
 (in-package "ACL2")
 
+;; See also basic-rules.lisp
+
 (defthm equal-of-+-combine-constants-alt
   (implies (syntaxp (and (quotep k1)
                          (quotep k2)))

books/kestrel/axe/basic-rules.lisp

@@ -12,14 +12,17 @@
 
 (in-package "ACL2")
 
-(include-book "kestrel/utilities/if" :dir :system)
+;(include-book "kestrel/utilities/if" :dir :system) ; drop?
 (include-book "kestrel/booleans/bool-fix-def" :dir :system)
+(local (include-book "kestrel/arithmetic-light/mod" :dir :system))
 
 ;; TODO: Rephrase some of these
 
 ;;theorems about built-in ACL2 functions.  Many of these are things that ACL2
 ;;knows by type reasoning (but Axe does not have type reasoning).
 
+;; See also arithmetic-rules-axe.lisp
+
 (defthmd rationalp-of-len
   (rationalp (len x)))
 
@@ -31,6 +34,12 @@
 (defthmd acl2-numberp-of-*
   (acl2-numberp (* x y)))
 
+;dup
+(defthm integerp-of-*
+  (implies (and (integerp x)
+                (integerp y))
+           (integerp (* x y))))
+
 (defthmd acl2-numberp-of-unary--
   (acl2-numberp (unary-- x)))
 
@@ -189,3 +198,12 @@
 (defthmd acl2-numberp-when-signed-byte-p
   (implies (signed-byte-p size x) ; size is a free var
            (acl2-numberp x)))
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
+;dup
+(defthm integerp-of-mod
+  (implies (integerp y)
+           (equal (integerp (mod x y))
+                  (integerp (fix x))))
+  :hints (("Goal" :in-theory (enable mod))))

books/kestrel/axe/def-simplified.lisp

@@ -29,6 +29,7 @@
 (include-book "choose-rules")
 ;(include-book "rules-in-rule-lists")
 ;; The rest of these include-books are to bring in everything included in def-simplified-rules below:
+(include-book "kestrel/utilities/if" :dir :system)
 (include-book "rules1") ; for BV-ARRAY-CLEAR-OF-BV-ARRAY-CLEAR-SAME
 (include-book "basic-rules") ;for equal-same
 (include-book "boolean-rules-axe") ;for MYIF-BECOMES-BOOLIF-AXE

books/kestrel/axe/rule-lists.lisp

@@ -189,9 +189,6 @@
             not-of-if
 
             fix-when-acl2-numberp
-            acl2-numberp-of-+
-            acl2-numberp-of-fix
-            integerp-of-ifix
             = ; introduces EQUAL
             eql ; introduces EQUAL ; EQL can arise from CASE
             eq ; introduces EQUAL
@@ -203,7 +200,7 @@
             double-rewrite ; todo: or remove these when we make the axe-rules
             return-last
 
-            not-stringp-of-cons)
+            )
           (mv-nth-rules)
           (boolean-rules-safe)
           (booleanp-rules)))
@@ -252,7 +249,24 @@
     integerp-of--
     integerp-of-+
 
-    integerp-when-unsigned-byte-p-free))
+    integerp-when-unsigned-byte-p-free
+
+    ;; todo: acl2-numberp-when-integerp
+    ;; todo: acl2-numberp-when-natp ?
+    acl2-numberp-of-fix
+    acl2-numberp-of-+
+    acl2-numberp-of-*
+    acl2-numberp-of-unary--
+    acl2-numberp-of-mod
+    acl2-numberp-of-floor
+
+    integerp-of-ifix
+    integerp-of-+
+    integerp-of-*
+    integerp-of-mod
+
+    not-stringp-of-cons
+    ))
 
 (defun safe-trim-rules ()
   (declare (xargs :guard t))
@@ -2216,6 +2230,7 @@
 ;;normalize boolif nests that are really ands?
 
 ;; TODO: add many more rules to this?
+; not used?
 (defun arithmetic-rules ()
   (declare (xargs :guard t))
   '(fold-consts-in-+
@@ -2284,10 +2299,10 @@
     bvplus-of-unary-minus
     bvchop-of-+-becomes-bvplus
     ;move these to type-rules:
-    integerp-of-*
-    acl2-numberp-of-+
-    acl2-numberp-of-*
-    acl2-numberp-of-unary--
+    ;; integerp-of-*
+    ;; acl2-numberp-of-+
+    ;; acl2-numberp-of-*
+    ;; acl2-numberp-of-unary--
     fix
     integerp-of-+-when-integerp-1-cheap
     mod-becomes-bvchop-when-power-of-2p

books/kestrel/axe/rules-in-rule-lists.lisp

@@ -15,6 +15,7 @@
 ;; This book is intended to bring in all the rules that are in rule-lists.lisp.
 ;; See also rules-in-rule-lists-jvm.lisp.
 
+(include-book "kestrel/utilities/if" :dir :system)
 (include-book "kestrel/arithmetic-light/mod2" :dir :system)
 (include-book "basic-rules")
 (include-book "if-rules")

books/kestrel/axe/tactic-prover.lisp

@@ -46,6 +46,8 @@
 (include-book "kestrel/bv/unsigned-byte-p-forced-rules" :dir :system)
 (include-book "bv-rules-axe0")
 (include-book "bv-rules-axe")
+(include-book "basic-rules")
+(include-book "arithmetic-rules-axe")
 (include-book "bv-array-rules-axe") ; not all are needed, but we need integerp-of-bv-array-read
 (include-book "bv-intro-rules")
 (include-book "kestrel/bv-lists/bv-array-read-rules" :dir :system) ; for UNSIGNED-BYTE-P-FORCED-OF-BV-ARRAY-READ