PVS_theories/fp_lemmas.pvs

+fp_lemmas
+ [b,p:above(1),
+   alpha,E_max:integer,
+   E_min:{i:integer|E_max>i}]:THEORY
+
+BEGIN
+
+
+IMPORTING float@IEEE_854_defs[b,p,alpha,E_max,E_min]
+
+infinite_not_zero: LEMMA FORALL (x:fp_num): infinite?(x) => NOT zero?(x)
+
+%finite_mul_1: LEMMA FORALL(x:{fp:fp_num|finite?(fp)},mode:rounding_mode): finite?(fp_mul(x,real_to_fp(1),mode))
+
+op_fin_inf: LEMMA FORALL (mode:rounding_mode, x:{fp:fp_num|finite?(fp)}, y:{fp:fp_num| finite?(fp)},op:{op:fp_ops|zero?(y) OR (zero?(x) AND zero?(y)) => NOT div?(op)}):
+finite?(fp_op(op,x,y,mode)) OR infinite?(fp_op(op,x,y,mode))
+
+op_add_inf_fin: LEMMA FORALL (mode:rounding_mode, x:{fp:fp_num|finite?(fp) OR infinite?(fp)},y:{fp:fp_num| finite?(fp) OR infinite?(fp)}): infinite?(x) XOR infinite?(y) => finite?(fp_add(x,y,mode)) OR infinite?(fp_add(x,y,mode)) 
+
+op_add_inf_fin_l: LEMMA FORALL (mode:rounding_mode, x:{fp:fp_num|finite?(fp) OR infinite?(fp)},y:{fp:fp_num| finite?(fp)}): finite?(fp_add(x,y,mode)) OR infinite?(fp_add(x,y,mode)) 
+
+op_add_inf_fin_r: LEMMA FORALL (mode:rounding_mode, x:{fp:fp_num|finite?(fp) OR infinite?(fp)},y:{fp:fp_num| finite?(fp)}): finite?(fp_add(y,x,mode)) OR infinite?(fp_add(y,x,mode)) 
+
+op_sub_inf_fin_l: LEMMA FORALL (mode:rounding_mode, x:{fp:fp_num|finite?(fp) OR infinite?(fp)},y:{fp:fp_num| finite?(fp)}): finite?(fp_sub(x,y,mode)) OR infinite?(fp_sub(x,y,mode)) 
+
+op_sub_inf_fin_r: LEMMA FORALL (mode:rounding_mode, x:{fp:fp_num|finite?(fp) OR infinite?(fp)},y:{fp:fp_num| finite?(fp)}): finite?(fp_sub(y,x,mode)) OR infinite?(fp_sub(y,x,mode))
+
+op_mul_inf_fin_l: LEMMA FORALL (mode:rounding_mode, x:{fp:fp_num|finite?(fp) OR infinite?(fp)},y:{fp:fp_num| finite?(fp) AND (infinite?(x) => NOT zero?(fp))}): finite?(fp_mul(y,x,mode)) OR infinite?(fp_mul(y,x,mode))
+
+op_mul_inf_fin_r: LEMMA FORALL (mode:rounding_mode, x:{fp:fp_num|finite?(fp) OR infinite?(fp)},y:{fp:fp_num| finite?(fp) AND (infinite?(x) => NOT zero?(fp))}): finite?(fp_mul(x,y,mode)) OR infinite?(fp_mul(x,y,mode))
+
+op_div_inf_fin_l: LEMMA FORALL (mode:rounding_mode, x:{fp:fp_num|finite?(fp) OR infinite?(fp)},y:{fp:fp_num| finite?(fp) AND NOT zero?(fp)}): finite?(fp_div(x,y,mode)) OR infinite?(fp_div(x,y,mode))
+
+op_div_inf_fin_r: LEMMA FORALL (mode:rounding_mode, x:{fp:fp_num|finite?(fp) AND NOT zero?(fp)},y:{fp:fp_num| finite?(fp) OR infinite?(fp)}): finite?(fp_div(y,x,mode)) OR infinite?(fp_div(y,x,mode))
+
+op_sqrt_inf_fin: LEMMA FORALL (mode:rounding_mode, x:{fp:fp_num|(finite?(fp) AND sign(fp) = pos) OR (infinite?(fp) AND i_sign(fp) = pos)}): finite?(fp_sqrt(x,mode)) OR infinite?(fp_sqrt(x,mode))
+
+
+END fp_lemmas

PVS_theories/overload.pvs

+overload[b,p:above(1),
+   alpha,E_max:integer,
+   E_min:{i:integer|E_max>i},
+(IMPORTING float@enumerated_type_defs)r_mode:rounding_mode]:THEORY
+
+BEGIN
+
+IMPORTING fp_lemmas[b,p,alpha,E_max,E_min]
+
+x,y: VAR fp_num
+n:VAR nat
+
+-(x,y):fp_num = fp_sub(x,y,r_mode);
++(x,y):fp_num = fp_add(x,y,r_mode);
+*(x,y):fp_num = fp_mul(x,y,r_mode);
+/(x,y):fp_num = fp_div(x,y,r_mode);
+sqrt(x):fp_num = fp_sqrt(x,r_mode);
+-(x):fp_num = toggle_sign(x);
+
+-(x:fp_num,y:real):fp_num = x-real_to_fp(y);
++(x:fp_num,y:real):fp_num = x+real_to_fp(y);
+*(x:fp_num,y:real):fp_num = x*real_to_fp(y);
+/(x:fp_num,y:real):fp_num = x/real_to_fp(y);
+
+-(x:real,y:fp_num):fp_num = real_to_fp(x)-y;
++(x:real,y:fp_num):fp_num = real_to_fp(x)+y;
+*(x:real,y:fp_num):fp_num = real_to_fp(x)*y;
+/(x:real,y:fp_num):fp_num = real_to_fp(x)/y;
+
+
+<(x,y:{fp:fp_num|finite?(fp) OR infinite?(fp)}):bool = n_value(x) < n_value(y);
+<=(x,y:{fp:fp_num|finite?(fp) OR infinite?(fp)}):bool = n_value(x) <= n_value(y);
+>(x,y:{fp:fp_num|finite?(fp) OR infinite?(fp)}):bool = n_value(x) > n_value(y);
+>=(x,y:{fp:fp_num|finite?(fp) OR infinite?(fp)}):bool = n_value(x) >= n_value(y);
+=(x,y:{fp:fp_num|finite?(fp) OR infinite?(fp)}):bool = n_value(x) = n_value(y);
+/=(x,y:{fp:fp_num|finite?(fp) OR infinite?(fp)}):bool = n_value(x) /= n_value(y);
+
+<(x:real,y:{fp:fp_num|finite?(fp) OR infinite?(fp)}):bool = real_to_fp(x) < y;
+<=(x:real,y:{fp:fp_num|finite?(fp) OR infinite?(fp)}):bool = real_to_fp(x) <= y;
+>(x:real,y:{fp:fp_num|finite?(fp) OR infinite?(fp)}):bool = real_to_fp(x) > y;
+>=(x:real,y:{fp:fp_num|finite?(fp) OR infinite?(fp)}):bool = real_to_fp(x) >= y;
+=(x:real,y:{fp:fp_num|finite?(fp) OR infinite?(fp)}):bool = real_to_fp(x) = y;
+/=(x:real,y:{fp:fp_num|finite?(fp) OR infinite?(fp)}):bool = real_to_fp(x) /= y;
+
+<(x:{fp:fp_num|finite?(fp) OR infinite?(fp)},y:real):bool = x < real_to_fp(y);
+<=(x:{fp:fp_num|finite?(fp) OR infinite?(fp)},y:real):bool = x <= real_to_fp(y);
+>(x:{fp:fp_num|finite?(fp) OR infinite?(fp)},y:real):bool = x > real_to_fp(y);
+>=(x:{fp:fp_num|finite?(fp) OR infinite?(fp)},y:real):bool = x >= real_to_fp(y);
+=(x:{fp:fp_num|finite?(fp) OR infinite?(fp)},y:real):bool = x = real_to_fp(y);
+/=(x:{fp:fp_num|finite?(fp) OR infinite?(fp)},y:real):bool = x /= real_to_fp(y);
+
+expt(x,n): RECURSIVE fp_num =
+  IF n = 0 THEN real_to_fp(1)
+  ELSE x * expt(x, n-1)
+  ENDIF
+MEASURE n;
+
+^(x: fp_num, i:int): fp_num
+    = IF i >= 0 THEN expt(x, i) ELSE real_to_fp(1)/expt(x, -i) ENDIF
+END overload

PVS_theories/single.pvs

+single: THEORY
+
+BEGIN
+ 
+IMPORTING float@enumerated_type_defs
+IMPORTING overload[2,24,192,127,-126,to_nearest]
+
+single: TYPE = {fp:fp_num|finite?(fp) OR infinite?(fp)}
+single_finite: TYPE = {fp:fp_num|finite?(fp)}
+
+END single