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
|
ExpLog: THEORY
BEGIN
IMPORTING Real
% do not edit above this line
IMPORTING lnexp@ln_exp
% Why3 exp
exp(x:real): MACRO real = exp(x)
% Why3 exp_zero
exp_zero: LEMMA (exp(0) = 1)
% Why3 exp_sum
exp_sum: LEMMA FORALL (x:real, y:real): (exp((x + y)) = (exp(x) * exp(y)))
% Why3 e
e: real = exp(1)
log_total(x: real): real
% Why3 log
log(x:real): MACRO real = IF x > 0 THEN ln(x) ELSE log_total(x) ENDIF
% Why3 log_one
log_one: LEMMA (log(1) = 0)
% Why3 log_mul
log_mul: LEMMA FORALL (x:real, y:real): ((x > 0) AND (y > 0)) =>
(log((x * y)) = (log(x) + log(y)))
% Why3 log_exp
log_exp: LEMMA FORALL (x:real): (log(exp(x)) = x)
% Why3 exp_log
exp_log: LEMMA FORALL (x:real): (x > 0) => (exp(log(x)) = x)
% Why3 log2
log2(x:real): real = Real.infix_sl(log(x), log(2))
% Why3 log10
log10(x:real): real = Real.infix_sl(log(x), log(10))
END ExpLog
|
