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
89
90
91
92
93
94
|
; Copyright (C) 2007 by Shant Harutunian
; License: A 3-clause BSD license. See the LICENSE file distributed with ACL2.
(in-package "ACL2")
(include-book "arith-nsa4")
(defstub eexp (x) t)
(defaxiom eexp-type
(implies
(realp x)
(and
(<= 0 (eexp x))
(realp (eexp x))))
:rule-classes :type-prescription)
(defaxiom eexp-standard-thm
(implies
(and
(realp x)
(standard-numberp x))
(standard-numberp (eexp x)))
:rule-classes :type-prescription)
(defaxiom eexp-standard-part-thm
(implies
(and
(realp x)
(i-limited x))
(equal (standard-part (eexp x))
(eexp (standard-part x)))))
(defaxiom eexp-i-limited-thm
(implies
(and
(realp x)
(i-limited x))
(i-limited (eexp x)))
:rule-classes ((:type-prescription) (:rewrite)))
(defaxiom eexp-0
(equal (eexp 0)
1))
(defaxiom eexp-monotone
(implies
(and
(realp x)
(realp y)
(< x y))
(< (eexp x) (eexp y))))
(defaxiom eexp-pos-arg
(implies
(and
(realp x)
(< 0 x))
(< 1 (eexp x)))
:rule-classes ((:linear) (:type-prescription)))
(defaxiom eexp-neg-arg
(implies
(and
(realp x)
(< x 0))
(< (eexp x) 1))
:rule-classes :linear)
(defaxiom 1+x-<=eexp-thm
(implies
(and
(realp x)
(<= 0 x))
(<= (+ 1 x)
(eexp x)))
:rule-classes :linear)
(defaxiom eexp-plus-thm
(implies
(and
(realp x)
(realp y))
(equal (* (eexp x) (eexp y))
(eexp (+ x y)))))
(defthm eexp-plus-thm-3way
(implies
(and
(realp x)
(realp y)
(realp z))
(equal (* (eexp x) (eexp y) z)
(* (eexp (+ x y)) z))))
|
