From afbbb947921dd93024a616086d5f75b581d70437 Mon Sep 17 00:00:00 2001
From: Masaya Tojo <masaya@tojo.tokyo>
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