CommonLispにもML系Matchがないのか。
(in-package "ACL2") (defun not-3 (x) (cond ((equal x "yes") "no") ((equal x "no") "yes") ((equal x "maybe") "maybe"))) (defun and-3 (x y) (cond ((and (equal x "yes") (equal y "yes")) "yes") ((and (equal x "yes") (equal y "no")) "no") ((and (equal x "yes") (equal y "maybe")) "maybe") ((and (equal x "no") (equal y "yes")) "no") ((and (equal x "no") (equal y "no")) "no") ((and (equal x "no") (equal y "maybe")) "no") ((and (equal x "maybe") (equal y "yes")) "maybe") ((and (equal x "maybe") (equal y "no")) "no") ((and (equal x "maybe") (equal y "maybe")) "maybe"))) (defun or-3 (x y) (cond ((and (equal x "yes") (equal y "yes")) "yes") ((and (equal x "yes") (equal y "no")) "yes") ((and (equal x "yes") (equal y "maybe")) "yes") ((and (equal x "no") (equal y "yes")) "yes") ((and (equal x "no") (equal y "no")) "no") ((and (equal x "no") (equal y "maybe")) "maybe") ((and (equal x "maybe") (equal y "yes")) "yes") ((and (equal x "maybe") (equal y "no")) "maybe") ((and (equal x "maybe") (equal y "maybe")) "maybe"))) (defthm and-3-comm (iff (and-3 x y) (and-3 y x))) (defthm and-3-ldistr-or-3 (iff (and-3 t (or-3 u v)) (or-3 (and-3 t u) (and-3 t v)))) (defthm and-3-rdistr-or-3 (iff (and-3 (or-3 t u) v) (or-3 (and-3 t v) (and-3 u v))))
全部自動で証明までできてる。