/usr/share/acl2-7.1/books/arithmetic/abs.lisp is in acl2-books-source 7.1-1.
This file is owned by root:root, with mode 0o644.
The actual contents of the file can be viewed below.
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 | ;;; Contributed by Ruben A. Gamboa
; Copyright (C) 2014, University of Wyoming
; All rights reserved.
; License: A 3-clause BSD license. See the LICENSE file distributed with ACL2.
(in-package "ACL2")
;;; The absolute-value function has many useful properties, but ACL2
;;; doesn't know about them. Instead, it likes to explode abs(x) into
;;; the two cases x<0 and x>=0, and that often leads to unnecessary
;;; case explosions. In this book, we prove the more useful lemmas
;;; about abs.
(include-book "top")
;;; We start with |x*y| = |x| * |y|. This is actually a dangerous
;;; lemma, sometimes, so we often disable it.
(defthm abs-*
(implies (and (real/rationalp x) (real/rationalp y))
(equal (abs (* x y))
(* (abs x) (abs y)))))
;;; An obvious lemma that ACL2 doesn't know is that |-x| = |x|.
(defthm abs-uminus
(equal (abs (- x))
(abs (fix x))))
;;; And |x| is always real, so long as x is real (which is should be
;;; from the guards).
(defthm realp-abs
(implies (real/rationalp x)
(real/rationalp (abs x))))
;;; Similarly, abs is always numeric.
(defthm numberp-abs
(implies (acl2-numberp x)
(acl2-numberp (abs x))))
;;; |x| = x when x is a non-negative real.
(defthm abs-x->-0
(implies (and (real/rationalp x)
(<= 0 x))
(equal (abs x) x)))
;;; If x is real and non-zero, then |x| is positive.
(defthm abs-x-=-0-iff-x=0
(implies (and (real/rationalp x)
(not (= 0 x)))
(< 0 (abs x))))
;;; And no matter what, |x|>=0.
(defthm not-abs-x-<-0
(not (< (abs x) 0))
:rule-classes (:rewrite :type-prescription))
;;; When you see a term |x| in an expression and you want to replace
;;; it with a new variable x1, keep in mind that x1>=0.
(defthm abs-x-generalize-weak
(implies (real/rationalp x)
(and (<= 0 (abs x))
(real/rationalp (abs x))))
:rule-classes (:generalize :rewrite))
;;; Moreover, if you know x is non-zero, when you generalize |x| with
;;; x1, you can assume that x1>0.
(defthm abs-x-generalize-strong
(implies (and (real/rationalp x)
(not (equal x 0)))
(< 0 (abs x)))
:rule-classes (:generalize :rewrite))
;;; |x+y| <= |x| + |y|.
(defthm abs-triangle
(<= (abs (+ x y)) (+ (abs x) (abs y))))
(in-theory (disable abs))
|