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
|
;;; 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.
;;; This book develops the (very small) theory of the sum of a list of
;;; numbers. It is used to develop the theory of series from
;;; sequences in other books.
(in-package "ACL2")
;; First, the definition of sumlist -- it's the obvious defun :-)
(defun sumlist (x)
(if (consp x)
(+ (car x)
(sumlist (cdr x)))
0))
;; ACL2 can conclude that sumlist is a numeric function. We'd like
;; for it to know that when the list contains only real numbers, its
;; sum is also a real number.
(defthm rationalp-sumlist
(implies (rational-listp x)
(rationalp (sumlist x))))
#+:non-standard-analysis
(defthm realp-sumlist
(implies (real-listp x)
(realp (sumlist x))))
;; This is the main lemma. The sum of a list can be computed by
;; splitting the list up into two parts and adding each part separately.
(defthm sumlist-append
(equal (sumlist (append x y))
(+ (sumlist x) (sumlist y))))
|
