-
Notifications
You must be signed in to change notification settings - Fork 50
/
Copy pathabs_lems.pvs
117 lines (78 loc) · 3.13 KB
/
abs_lems.pvs
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
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
abs_lems : THEORY
BEGIN
x,y : VAR real
t,a,b: VAR real
z : VAR nzreal
n : VAR nat
nnx : VAR nnreal
IMPORTING sq,root
abs_eq_0 : LEMMA abs(x) = 0 IFF x = 0
abs_0 : LEMMA abs(0) = 0
abs_nat : LEMMA abs(n) = n
abs_nnreal : LEMMA abs(nnx) = nnx
abs_diff : LEMMA abs(x) - abs(y) <= abs(x - y)
abs_neg : LEMMA abs(-x) = abs(x)
abs_diff_commute : LEMMA abs(x - y) = abs(y - x)
abs_diff_0 : LEMMA x = y IFF abs(x - y) = 0
abs_add_pos : LEMMA
x*y >= 0 IMPLIES
abs(x+y) = abs(x)+abs(y)
triangle2 : LEMMA abs(x - t) < a AND abs(x - y) < b
IMPLIES abs(t - y) < a + b
abs_sq : LEMMA abs(sq(a)) = sq(a)
abs_lt : LEMMA abs(x) < a IFF x > -a AND x < a
abs_le : LEMMA abs(x) <= a IFF x >= -a AND x <= a
abs_gt : LEMMA abs(x) > a IFF x < -a OR x > a
abs_ge : LEMMA abs(x) >= a IFF x <= -a OR x >= a
abs_pos : LEMMA abs(x) > 0 IFF x /= 0
gt_abs : LEMMA a > abs(x) IFF x > -a AND x < a
ge_abs : LEMMA a >= abs(x) IFF x >= -a AND x <= a
lt_abs : LEMMA a < abs(x) IFF x < -a OR x > a
le_abs : LEMMA a <= abs(x) IFF x <= -a OR x >= a
pos_abs : LEMMA 0 < abs(x) IFF x /= 0
diff_center : LEMMA abs(x - a) <= nnx IMPLIES abs(x) <= abs(a) + nnx
% -------- The following lemmas were suggested by Ben Hocking
abs_bounding_le: LEMMA
FORALL(a: real, nnx: nnreal, b: real, nny: nnreal):
abs(a) <= nnx AND abs(b) <= nny IMPLIES
-(nnx * nny) <= (a * b) AND
(a * b) <= (nnx * nny)
abs_bounding_lt: LEMMA
FORALL(a: real, nnx: nnreal, b: real, nny: nnreal):
abs(a) < nnx AND abs(b) < nny IMPLIES
-(nnx * nny) < (a * b) AND
(a * b) < (nnx * nny)
% -------- abs(f) and abs of linear function: minimum property ----
f: VAR [real -> real]
m: VAR real
abs_mono_inc: LEMMA
m*t + b = 0 AND
t <= x AND x <= y
IMPLIES
abs(m*x+b) <= abs(m*y+b)
abs_mono_dec: LEMMA
m*t + b = 0 AND
x <= y AND y <= t
IMPLIES
abs(m*x+b) >= abs(m*y+b)
AUTO_REWRITE+ abs_0
AUTO_REWRITE+ abs_nat
AUTO_REWRITE- abs_diff_commute
abs_root: LEMMA n>0 AND (x<0 IMPLIES odd?(n))
IMPLIES abs(root_real(x)(n)) =
root_real(abs(x))(n)
% ------------ properties about distances ----------------------------
abs_dist: LEMMA
FORALL(x1,x2: real, y1: nonneg_real):
abs(x1-x2) <= y1
IMPLIES abs(x1) <= abs(x2) + y1
abs_triang: LEMMA
FORALL(x1,x2,x3: real, y1,y2: nonneg_real):
abs(x1-x2) <= y1 AND
abs(x2-x3) <= y2
IMPLIES abs(x1-x3) <= y1+y2
abs_dist_other: LEMMA
FORALL(x1,x3,x2: real, y1: nonneg_real):
abs(x1-x2) <= y1
IMPLIES abs(x1-x3) <= y1 + abs(x3-x2)
END abs_lems