From afbbb947921dd93024a616086d5f75b581d70437 Mon Sep 17 00:00:00 2001 From: Masaya Tojo Date: Fri, 27 Aug 2021 01:04:05 +0900 Subject: units: Add units.lisp --- units.lisp | 39 +++++++++++++++++++++++++++++++++++++++ 1 file changed, 39 insertions(+) create mode 100644 units.lisp diff --git a/units.lisp b/units.lisp new file mode 100644 index 0000000..4b353e1 --- /dev/null +++ b/units.lisp @@ -0,0 +1,39 @@ +(defun m (x) + x) + +(defun s (x) + x) + +(defthm m+m + (equal (+ (m x) (m y)) + (m (+ x y)))) + +(defthm s+s + (equal (+ (s x) (s y)) + (s (+ x y)))) + +(defun m/s (x) + x) + +(defthm m/s+m/s + (equal (+ (m/s x) (m/s y)) + (m/s (+ x y)))) + +(defthm m/s*s + (equal (* (m/s x) (s y)) + (m (* x y)))) + +(defthm m*/s + (equal (* (m x) (/ (s y))) + (m/s (* x (/ y))))) + +(defthm m*/m/s + (equal (* (m x) (/ (m/s y))) + (m (* x (/ y))))) + +(in-theory (disable m s m/s)) + +(defthm test + (equal (/ (m x) (/ (m y) (s z))) + (m (/ x (/ y z)))) + :rule-classes nil) -- cgit v1.2.3