-
Notifications
You must be signed in to change notification settings - Fork 50
/
Copy pathreal_fun_ops_aux.pvs
54 lines (44 loc) · 2.01 KB
/
real_fun_ops_aux.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
%------------------------------------------------------------------------------
% Arithmetic Operations defined on functions [T->real]
%
% Author: David Lester, Manchester University
%
% Version 1.0 14/06/09 Initial Version
%------------------------------------------------------------------------------
real_fun_ops_aux[T:TYPE]: THEORY
BEGIN
IMPORTING real_fun_ops, sq
f,f1,f2: VAR [T->real]
f3: VAR [T -> nzreal]
F: VAR sequence[[T->real]]
x,y: VAR T
nnc: VAR nnreal
npc: VAR npreal
a,c: VAR real
n,i: VAR nat
sq(f): [T->nnreal] = lambda x: sq(f(x))
min(f1,f2):[T->real] = lambda x: min(f1(x),f2(x))
max(f1,f2):[T->real] = lambda x: max(f1(x),f2(x))
minus(f): [T->nnreal] = lambda x: -min(f(x),0)
plus(f): [T->nnreal] = lambda x: max(f(x),0)
maximum(F,n): RECURSIVE [T->real]
= IF n = 0 THEN F(0) ELSE max(F(n),maximum(F,n-1)) ENDIF MEASURE n
minimum(F,n): RECURSIVE [T->real]
= IF n = 0 THEN F(0) ELSE min(F(n),minimum(F,n-1)) ENDIF MEASURE n
plus_minus_def: LEMMA f = plus(f) - minus(f)
max_plus_min: LEMMA max(f1,f2)+min(f1,f2) = f1+f2
max_minus_min: LEMMA max(f1,f2)-min(f1,f2) = abs(f1-f2)
max_def: LEMMA max(f1,f2) = (1/2)*(f1+f2+abs(f1-f2))
min_def: LEMMA min(f1,f2) = (1/2)*(f1+f2-abs(f1-f2))
prod_def: LEMMA *(f1,f2) = (1/4)*(sq(f1+f2)-sq(f1-f2))
plus_plus: LEMMA plus(plus(f)) = plus(f)
plus_minus: LEMMA plus(minus(f)) = minus(f)
minus_plus: LEMMA minus(plus(f)) = const_fun(0)
minus_minus: LEMMA minus(minus(f)) = const_fun(0)
plus_scal: LEMMA plus(c*f) = IF c>=0 THEN c*plus(f) ELSE -c*minus(f) ENDIF
minus_scal: LEMMA minus(c*f) = IF c>=0 THEN c*minus(f) ELSE -c*plus(f) ENDIF
maximum_def1: LEMMA i <= n => FORALL x: F(i)(x) <= maximum(F,n)(x)
maximum_def2: LEMMA EXISTS i: i <= n AND maximum(F,n)(x) = F(i)(x)
minimum_def1: LEMMA i <= n => FORALL x: minimum(F,n)(x) <= F(i)(x)
minimum_def2: LEMMA EXISTS i: i <= n AND minimum(F,n)(x) = F(i)(x)
END real_fun_ops_aux