%Patch files loaded: (patch2) version 2.376 $$$IEEE_854.pvs IEEE_854 [b,p:above(1),alpha,E_max,E_min:integer]: THEORY %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % This theory defines the representation and basic operations for % arbitrary precision IEEE-854 floating point numbers. It also % introduces the required assumption for arbitrary precision % IEEE-854 floating point numbers. % % Example use: % % To define IEEE-754 single-precision operations use the following % importing: % % IMPORTING IEEE_854[2,24,192,127,-126] % % Author: % Paul S. Miner | email: p.s.miner@larc.nasa.gov % 1 South Wright St. / MS 130 | fax: (804) 864-4234 % NASA Langley Research Center | phone: (804) 864-6201 % Hampton, Virginia 23681 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% BEGIN %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Representation assumptions (from section 3.1 of IEEE-854) ASSUMING Base_values: ASSUMPTION b=2 or b=10 Exponent_range: ASSUMPTION (E_max - E_min)/p > 5 %10 % may be 5 Significand_size: ASSUMPTION b^(p-1)>=10^5 % Uncomment the following, if you wish to include the suggestion % about exponent balance . E_balance: ASSUMPTION IF b < 4 THEN E_max + E_min = 1 ELSE E_max + E_min = 0 ENDIF % Although not mentioned explicitly as a parameter. We need the following % value for adjusting the exponent of overflow and underflow results when the % corresponing traps are enabled. % Section 7.3 of IEEE-854 states: `` The exponent adjustment $\alpha$ % for a precision shall be chosen to be approximately % $3\times(\Emax - \Emin)/4$ for that precision and should be % divisible by twelve.'' Exponent_Adjustment: ASSUMPTION abs(alpha - (3 * (E_max - E_min) / 4)) <= 6 & integer?(alpha / 12) ENDASSUMING %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Assumption about balanced exponents as given in standard % (comment out if you do not desire this constraint) Exponent_balance: LEMMA b^(E_max+E_min) <4 & 4<=b^(E_max+E_min+1) %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % A useful consequence of the assumptions E_max_gt_E_min: lemma E_max > E_min % An illustrative example for HUG95 paper HUG_example: lemma 5*p < E_max-E_min => E_min < E_max % Simple examples showing how importing tccs may be automatically proven ex754_2:lemma (127 - (-126))/24 > 5 ex754_3: lemma 2^23 >=10^5 % Some beneficial consequences of assumption E_balance % (These cannot be proven without E_balance) E_min_neg: lemma E_min<0 E_max_pos: lemma E_max>0 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% Importing IEEE_854_defs[b,p,alpha,E_max,E_min] END IEEE_854 $$$IEEE_854.prf (IEEE_854 (|Exponent_range_TCC1| "" (TCC) NIL) (|Significand_size_TCC1| "" (TCC :DEFS !) NIL) (|Exponent_balance_TCC1| "" (TCC :DEFS !) NIL) (|Exponent_balance_TCC2| "" (TCC :DEFS !) NIL) (|Exponent_balance| "" (LEMMA "E_balance") (("" (LEMMA "expt_x1") (("" (INST?) (("" (LEMMA "expt_x0") (("" (INST?) (("" (GROUND) (("" (LEMMA "expt_plus") (("" (INST - "1" "E_max+E_min" "b") (("" (ASSERT) (("" (TYPEPRED "b") (("" (CASE "forall (i:above(1)): 4<=i*i") (("1" (INST?) (("1" (ASSERT) NIL))) ("2" (INDUCT "i" 1 "above_induction[1]") (("1" (ASSERT) NIL) ("2" (SKOSIMP*) (("2" (ASSERT) NIL))))))))))))))))))))))))))) (|E_max_gt_E_min| "" (LEMMA "Exponent_range") (("" (REWRITE "div_mult_pos_gt2") (("" (ASSERT) NIL))))) (|HUG_example| "" (GROUND) NIL) (|ex754_2| "" (ASSERT) NIL) (|ex754_3| "" (GRIND) NIL) (|E_min_neg| "" (LEMMA "E_balance") (("" (LEMMA "Exponent_range") (("" (REWRITE "div_mult_pos_gt2") (("" (GROUND) NIL))))))) (|E_max_pos| "" (LEMMA "E_balance") (("" (LEMMA "Exponent_range") (("" (REWRITE "div_mult_pos_gt2") (("" (GROUND) NIL))))))) (IMPORTING1_TCC1 "" (REWRITE "E_max_gt_E_min") NIL) (IMPORTING1_TCC2 "" (INST 1 "E_max - 1") NIL)) $$$IEEE_854_defs.pvs IEEE_854_defs [b,p:above(1), alpha,E_max:integer, E_min:{i:integer|E_max>i}]: THEORY BEGIN IMPORTING IEEE_854_values[b,p,E_max,E_min], IEEE_854_remainder[b,p,alpha,E_max,E_min], IEEE_854_fp_int[b,p,alpha,E_max,E_min], arithmetic_ops[b,p,alpha,E_max,E_min], comparison1[b,p,E_max,E_min], infinity_arithmetic[b,p,E_max,E_min], NaN_ops[b,p,E_max,E_min], enumerated_type_defs, sqrt %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % basic instruction schemata, ignoring exceptions for now % These functions are listed in section 5.1 of IEEE-854 fp,fp1,fp2: var fp_num mode: var rounding_mode % Addition operator fp_add(fp1, fp2, mode): fp_num = IF finite?(fp1) & finite?(fp2) THEN fp_op(add, fp1, fp2, mode) ELSIF NaN?(fp1) OR NaN?(fp2) THEN fp_nan(add, fp1, fp2) ELSE fp_add_inf(fp1, fp2) ENDIF % Addition operator with exceptions fp_add_x(fp1, fp2, mode): [fp_num, exception] = IF finite?(fp1) & finite?(fp2) THEN fp_op_x(add, fp1, fp2, mode) ELSIF NaN?(fp1) OR NaN?(fp2) THEN fp_nan_x(add, fp1, fp2) ELSE fp_add_inf_x(fp1, fp2) ENDIF fp_add_x_correct: lemma fp_add(fp1,fp2,mode) = proj_1(fp_add_x(fp1,fp2,mode)) % Subtraction Operator fp_sub(fp1, fp2, mode): fp_num = IF finite?(fp1) & finite?(fp2) THEN fp_op(sub, fp1, fp2, mode) ELSIF NaN?(fp1) OR NaN?(fp2) THEN fp_nan(sub, fp1, fp2) ELSE fp_sub_inf(fp1, fp2) ENDIF % Subtraction Operator with exceptions fp_sub_x(fp1, fp2, mode): [fp_num, exception] = IF finite?(fp1) & finite?(fp2) THEN fp_op_x(sub, fp1, fp2, mode) ELSIF NaN?(fp1) OR NaN?(fp2) THEN fp_nan_x(sub, fp1, fp2) ELSE fp_sub_inf_x(fp1, fp2) ENDIF % Excluding NaN operands, we should be able to prove a - b = a + (-b) % independent of the rounding mode fsub_alt_def: LEMMA NOT (NaN?(fp1) OR NaN?(fp2)) => fp_sub(fp1, fp2, mode) = fp_add(fp1, toggle_sign(fp2), mode) % Multiplication fp_mul(fp1, fp2, mode): fp_num = IF finite?(fp1) & finite?(fp2) THEN fp_op(mult, fp1, fp2, mode) ELSIF NaN?(fp1) OR NaN?(fp2) THEN fp_nan(mult, fp1, fp2) ELSE fp_mul_inf(fp1, fp2) ENDIF % Division fp_div(fp1, fp2, mode): fp_num = IF finite?(fp1) & finite?(fp2) THEN IF zero?(fp2) THEN IF zero?(fp1) THEN invalid ELSE infinite(mult_sign(fp1, fp2)) ENDIF ELSE fp_op(div, fp1, fp2, mode) ENDIF ELSIF NaN?(fp1) OR NaN?(fp2) THEN fp_nan(div, fp1, fp2) ELSE fp_div_inf(fp1, fp2) ENDIF % Remainder (independent of rounding mode) fp_rem(fp1, fp2): fp_num = IF finite?(fp1) & finite?(fp2) THEN IF zero?(fp2) THEN invalid ELSE REM(fp1, fp2) ENDIF ELSIF NaN?(fp1) OR NaN?(fp2) THEN fp_nan(div, fp1, fp2) ELSIF infinite?(fp1) THEN invalid ELSE fp1 ENDIF % Square root fp_sqrt(fp, mode): fp_num = IF NaN?(fp) THEN NaN_sqrt(fp) ELSIF zero?(fp) THEN fp ELSIF finite?(fp) THEN IF sign(fp) = pos THEN real_to_fp(fp_round(sqrt(value(fp)), mode)) ELSE invalid ENDIF ELSIF i_sign(fp) = pos THEN fp ELSE invalid ENDIF %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %% bug test spec, won't typecheck, %% cannot determine full theory instance % fp_id(fp):fp_num = % cases fp of % finite(s,e,d): fp, % infinite(s): fp, % NaN(sig,data):fp % endcases END IEEE_854_defs $$$IEEE_854_defs.prf (|IEEE_854_defs| (IMPORTING1_TCC1 "" (INST 1 "E_max - 1") NIL) (|fp_add_TCC1| "" (SKOSIMP*) NIL) (|fp_add_TCC2| "" (SKOSIMP*) NIL) (|fp_add_TCC3| "" (SKOSIMP*) (("" (ASSERT) NIL))) (|fp_add_TCC4| "" (SKOSIMP*) (("" (GROUND) NIL))) (|fp_add_x_correct| "" (SKOSIMP*) (("" (EXPAND "fp_add") (("" (EXPAND "fp_add_x") (("" (LIFT-IF) (("" (EXPAND "fp_nan") (("" (EXPAND "fp_nan_x") (("" (EXPAND "fp_add_inf") (("" (EXPAND "fp_add_inf_x") (("" (GROUND) (("" (EXPAND "fp_op") (("" (EXPAND "fp_op_x") (("" (EXPAND "real_to_fp_x") (("" (EXPAND "fp_round") (("" (EXPAND "fp_round_x") (("" (LIFT-IF) (("" (EXPAND "round_exceptions") (("" (PROPAX) NIL))))))))))))))))))))))))))))))))) (|fsub_alt_def| "" (SKOSIMP*) (("" (EXPAND "fp_sub") (("" (EXPAND "fp_add") (("" (REWRITE "toggle_finite") (("" (REWRITE "toggle_NaN") (("" (LIFT-IF) (("" (ASSERT) (("" (SPLIT) (("1" (FLATTEN) (("1" (EXPAND "fp_op") (("1" (EXPAND "apply") (("1" (REWRITE "value_toggle") (("1" (ASSERT) (("1" (LIFT-IF) (("1" (ASSERT) (("1" (GROUND) (("1" (EXPAND "signed_zero") (("1" (CASE "forall fp: zero?(toggle_sign(fp)) iff zero?(fp)") (("1" (INST?) (("1" (REPLACE -1) (("1" (CASE "forall (fin1,fin2: (finite?)): (sign(fin1) = sign(toggle_sign(fin2))) iff (sign(fin1) /= sign(fin2))") (("1" (INST?) (("1" (REPLACE -1) (("1" (PROPAX) NIL))))) ("2" (HIDE -1 -2 -3 -4 2 3 4) (("2" (SKOSIMP*) (("2" (EXPAND "toggle_sign") (("2" (TYPEPRED "sign(fin1!1)") (("2" (TYPEPRED "sign(fin2!1)") (("2" (GROUND) NIL))))))))))) ("3" (HIDE -1 -2 -3 -4 2 3 4) (("3" (SKOSIMP*) (("3" (REWRITE "toggle_finite") NIL))))))))))) ("2" (HIDE -1 -2 -3 2 3 4) (("2" (SKOSIMP*) (("2" (EXPAND "zero?") (("2" (REWRITE "toggle_finite") (("2" (REWRITE "value_toggle") (("2" (GROUND) NIL))))))))))))))))))))))))))))))) ("2" (FLATTEN) (("2" (REWRITE "fp_sub_inf_def") (("1" (GROUND) NIL) ("2" (GROUND) NIL))))))))))))))))))))) (|fp_div_TCC1| "" (SKOSIMP*) (("" (ASSERT) NIL))) (|fp_sqrt_TCC1| "" (SKOSIMP*) (("" (LEMMA "value_positive") (("" (INST?) (("" (ASSERT) NIL))))))) (|fp_sqrt_TCC2| "" (TCC) NIL)) $$$IEEE_854_values.pvs IEEE_854_values [b,p:above(1), E_max:integer, E_min:{i:integer|E_max>i}]: THEORY %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % This file defines the set of values that must be represented in each % supported precision of an instance of IEEE-854 % % Author: % Paul S. Miner | email: p.s.miner@larc.nasa.gov % 1 South Wright St. / MS 130 | fax: (804) 864-4234 % NASA Langley Research Center | phone: (804) 864-6201 % Hampton, Virginia 23681 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% BEGIN IMPORTING sum_hack, %for use until we have good summation library sum_lemmas[b], % these are more specialized enumerated_type_defs Exponent: type = {i:int| E_min <= i & i <= E_max} digits: type = [below(p)->below(b)] fp_num: datatype begin finite(sign:sign_rep,Exp:Exponent,d:digits):finite? infinite(i_sign:sign_rep): infinite? NaN(status:NaN_type, data:NaN_data): NaN? end fp_num % A mapping from finite floating point numbers to real numbers % This corresponds to the interpretation given in the standard % section 3.1 fin : var (finite?) value_digit(d:digits)(n:nat):nonneg_real = if n
0 ELSE FALSE ENDIF
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Some definitions and theorems to help illustrate the correctness
% of the definition of value.
% Maximum and Minimum representable values
max_significand:digits =
(lambda (i:below(p)): b-1)
min_significand: digits =
(LAMBDA (i: below(p)): IF i < p - 1 THEN 0 ELSE 1 ENDIF)
d_zero: digits = LAMBDA (i: below(p)): 0
m,n: var nat
Sum_value0: lemma Sum(n,value_digit(d_zero)) = 0
s: var sign_rep
E: var Exponent
zero_finite_d_zero: lemma zero?(finite(s,E,d_zero))
max_fp_pos : fp_num = finite(pos,E_max,max_significand)
min_fp_pos : fp_num = finite(pos,E_min,min_significand)
pos_zero : {fin|zero?(fin)}= finite(pos,E_min,d_zero)
max_fp_neg : fp_num = finite(neg,E_max,max_significand)
min_fp_neg : fp_num = finite(neg,E_min,min_significand)
neg_zero : {fin|zero?(fin)} = finite(neg,E_min,d_zero)
max_pos: posreal = value(max_fp_pos)
min_pos: posreal = value(min_fp_pos)
max_neg: negreal = value(max_fp_neg)
min_neg: negreal = value(min_fp_neg)
max_fp_correct: THEOREM
max_pos = b ^ (E_max +1) - b ^ (E_max + 1 - p)
min_fp_correct: THEOREM
value(min_fp_pos) = b ^ (E_min + 1 - p)
% Value of zero
value0: lemma value(fin)=0 iff d(fin)=d_zero
value_of_zero: THEOREM
value(pos_zero) = 0
% Normalization preserves the value
normal_value: lemma
value(fin) = value(normalize(fin))
% sign determines algebraic sign of value
value_positive: lemma
(sign(fin)=pos & not zero?(fin)) <=> value(fin)>0
value_negative: lemma
(sign(fin)=neg & not zero?(fin)) <=> value(fin)<0
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
finite_cover: lemma zero?(fin) or normal?(fin) or subnormal?(fin)
finite_disjoint1: lemma not (zero?(fin) & normal?(fin))
finite_disjoint2: lemma not (zero?(fin) & subnormal?(fin))
finite_disjoint3: lemma not (normal?(fin) & subnormal?(fin))
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
fp,fp1,fp2: var fp_num
% reverse the sign of a floating point number
toggle_sign(fp): fp_num
=
cases fp of
finite(s,e,d): finite(1-s,e,d),
infinite(s): infinite(1-s),
NaN(sig,data): fp
endcases
toggle_finite: lemma finite?(toggle_sign(fp)) iff finite?(fp)
toggle_infinite: lemma infinite?(toggle_sign(fp)) iff infinite?(fp)
toggle_NaN: lemma NaN?(toggle_sign(fp)) iff NaN?(fp)
value_toggle: lemma value(toggle_sign(fin)) = -value(fin)
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
toggle_d_normalize: lemma
d(normalize(toggle_sign(fin))) = d(normalize(fin))
toggle_Exp_normalize: lemma
Exp(normalize(toggle_sign(fin))) = Exp(normalize(fin))
toggle_zero?: lemma zero?(toggle_sign(fin)) iff zero?(fin)
toggle_normal?: lemma normal?(toggle_sign(fin)) iff normal?(fin)
toggle_subnormal?: lemma subnormal?(toggle_sign(fin)) iff subnormal?(fin)
% Sum lemmas
d: var digits
j : var nat
value_digit_le: lemma value_digit(d)(j) <= (b-1) * b^(-j)
Sum_d_lt_b: lemma Sum(j+1,value_digit(d)) <= b - b^(-j)
Sum_d_lt1: lemma d(0)=0 => Sum(j+1,value_digit(d)) <= 1-b^(-j)
Sum_d_ge1: lemma d(0)>0 => Sum(j+1,value_digit(d)) >= 1
value_sig_lt_b: lemma Sum(p,value_digit(d)) < b
value_sig_lt1: lemma d(0)=0 => Sum(p,value_digit(d)) < 1
value_sig_ge1: lemma d(0)>0 => Sum(p,value_digit(d)) >= 1
abs_value_fin: lemma
abs(value(fin)) = b^(Exp(fin)) * Sum(p,value_digit(d(fin)))
min_significand_min: lemma d/=d_zero =>
Sum(p,value_digit(min_significand))<= Sum(p,value_digit(d))
sign_normal: lemma sign(fin) = sign(normalize(fin))
value_normal: lemma normal?(fin) =>
b^E_min <= abs(value(fin)) & abs(value(fin)) <= max_pos
value_subnormal: lemma subnormal?(fin) =>
min_pos <= abs(value(fin)) & abs(value(fin)) < b^E_min
value_nonzero: lemma not zero?(fin) =>
min_pos <= abs(value(fin)) & abs(value(fin)) <= max_pos
%mod(floor(Sum(p, value_digit(d(normalize(fin!1)))) * b ^ x!1), b)
% = d(normalize(fin!1))(x!1)
scale_value(d,m)(n): nonneg_real = value_digit(d)(n) * b^m
scaled_Sum_int: lemma forall d,n:
forall (m:upto(n+1)): integer?(Sum(m,scale_value(d,n)))
scale_value_p(d)(n): nat = scale_value(d,p-1)(n)
i: var below(p)
scaled_Sum_i: lemma
Sum(n,value_digit(d))*b^(i) = Sum(n,scale_value(d,i))
scaled_Sum: lemma
Sum(n,value_digit(d))*b^(p-1) = Sum(n,scale_value_p(d))
floor_Sum: lemma
floor(Sum(p,value_digit(d)) * b^i) =
Sum(i+1,scale_value(d,i))
mod_Sum: lemma mod(Sum(i+1,scale_value(d,i)),b)=d(i)
%%%%%%%%%
%
% The next two declarations are here for importing purposes.
% A dummy fp_num to be used as a place holder. Any definition that
% returns holder is not yet finished.
holder:fp_num
% An undefined NaN for functions to return when the invalid exception
% should be raised. This serves as a placeholder until this specification
% accounts for exceptions.
%
invalid: (NaN?) = NaN(quiet,invalid_data)
END IEEE_854_values
$$$IEEE_854_values.prf
(|IEEE_854_values| (|digits_TCC1| "" (SUBTYPE-TCC) NIL)
(|digits_TCC2| "" (SUBTYPE-TCC) NIL)
(|value_digit_TCC1| "" (TCC :DEFS !) NIL)
(|value_digit_TCC2| "" (SKOSIMP*)
(("" (TYPEPRED "d!1(n!1)")
(("1" (LEMMA "expt_pos")
(("1" (INST?)
(("1" (REWRITE "pos_times_ge") (("1" (ASSERT) NIL)))
("2" (ASSERT) NIL)))))
("2" (PROPAX) NIL)))))
(|value_TCC1| "" (TCC :DEFS !) NIL)
(|shift_left_TCC1| "" (TCC :DEFS !) NIL)
(|shift_left_TCC2| "" (TCC :DEFS !) NIL)
(|normalize_TCC1| "" (TCC :DEFS !) NIL)
(|normalize_TCC2| "" (TCC :DEFS !) NIL)
(|normalize_TCC3| "" (TCC :DEFS !) NIL)
(|normalize_TCC4| "" (TCC :DEFS !) NIL)
(|normalize_idempotent| "" (SKOSIMP*)
(("" (CASE-REPLACE "fin!1=finite(sign(fin!1),Exp(fin!1),d(fin!1))")
(("1" (HIDE -1)
(("1"
(CASE "forall (s:sign_rep),(d:digits),(n:upto(E_max-E_min)):
normalize(normalize(finite(s,n+E_min,d)))=normalize(finite(s,n+E_min,d))")
(("1" (INST - "sign(fin!1)" "d(fin!1)" "Exp(fin!1)-E_min")
(("1" (ASSERT) NIL) ("2" (ASSERT) NIL)))
("2" (HIDE 2)
(("2" (INDUCT "n" 1 "upto_induction[E_max-E_min]")
(("1" (SKOSIMP*)
(("1" (EXPAND "normalize") (("1" (PROPAX) NIL)))))
("2" (SKOSIMP*)
(("2" (REWRITE "normalize" +)
(("2" (LIFT-IF)
(("2" (GROUND)
(("1" (REWRITE "normalize") NIL)
("2" (INST?) NIL)))))))))))))
("3" (ASSERT) NIL)))))
("2" (ASSERT) (("2" (REWRITE "fp_num_finite_eta") NIL)))))))
(|subnormal?_TCC1| "" (TCC :DEFS !) NIL)
(|normal?_TCC1| "" (TCC :DEFS !) NIL)
(|max_significand_TCC1| "" (TCC :DEFS !) NIL)
(|min_significand_TCC1| "" (TCC :DEFS !) NIL)
(|min_significand_TCC2| "" (TCC :DEFS !) NIL)
(|d_zero_TCC1| "" (TCC :DEFS !) NIL)
(|Sum_value0| "" (INDUCT-AND-SIMPLIFY "n") (("" (GRIND) NIL)))
(|zero_finite_d_zero| "" (GRIND :REWRITES "Sum_value0") NIL)
(|max_fp_pos_TCC1| "" (TCC :DEFS !) NIL)
(|min_fp_pos_TCC1| "" (TCC :DEFS !) NIL)
(|pos_zero_TCC1| "" (REWRITE "zero_finite_d_zero") NIL)
(|neg_zero_TCC1| "" (REWRITE "zero_finite_d_zero") NIL)
(|max_pos_TCC1| "" (TCC :DEFS !) NIL)
(|max_pos_TCC2| "" (EXPAND "value")
(("" (EXPAND "max_fp_pos")
(("" (EXPAND "pos")
(("" (REWRITE "expt_x0")
(("" (LEMMA "pos_times_gt")
(("" (ASSERT)
(("" (INST?)
(("" (ASSERT)
(("" (LEMMA "expt_pos")
(("" (INST?)
(("" (ASSERT)
((""
(CASE "Sum(p, value_digit(max_significand)) > 0")
(("1" (GROUND) NIL)
("2" (HIDE -1 -2 2)
(("2" (EXPAND "Sum")
(("2"
(ASSERT)
(("2"
(LEMMA "Sum_nonneg")
(("2"
(INST?)
(("2"
(REWRITE "value_digit")
(("2"
(REWRITE "max_significand")
(("2"
(LEMMA "expt_pos")
(("2"
(INST?)
(("2"
(LEMMA "pos_times_gt")
(("2"
(INST?)
(("2"
(GROUND)
NIL)))))))))))))))))))))))))))))))))))))))))))))))
(|min_pos_TCC1| "" (TCC) NIL)
(|min_pos_TCC2| "" (EXPAND "min_fp_pos")
(("" (EXPAND "value")
(("" (EXPAND "pos")
(("" (REWRITE "expt_x0")
(("" (LEMMA "expt_pos")
(("" (INST?)
(("1" (ASSERT)
(("1" (LEMMA "pos_times_gt")
(("1" (INST?)
(("1" (ASSERT)
(("1"
(CASE "Sum(p, value_digit(min_significand)) > 0")
(("1" (ASSERT) (("1" (ASSERT) NIL)))
("2" (HIDE -1 -2 2)
(("2" (EXPAND "Sum")
(("2" (LEMMA "Sum_nonneg")
(("2"
(INST?)
(("2"
(REWRITE "value_digit")
(("2"
(REWRITE "min_significand")
(("2"
(LEMMA "expt_pos")
(("2"
(INST?)
(("2"
(ASSERT)
NIL)))))))))))))))))))))))))))
("2" (ASSERT)
(("2" (SPLIT)
(("1" (ASSERT) NIL)
("2" (ASSERT) NIL)))))))))))))))))
(|max_neg_TCC1| "" (TCC :DEFS !) NIL)
(|max_neg_TCC2| "" (EXPAND "max_fp_neg")
(("" (EXPAND "value")
(("" (EXPAND "neg")
(("" (REWRITE "expt_x1")
(("" (LEMMA "expt_pos")
(("" (INST?)
(("1" (LEMMA "Sum_pos")
(("1" (INST?)
(("1" (ASSERT)
(("1" (LEMMA "pos_times_gt")
(("1" (INST?)
(("1" (GROUND)
(("1" (INST + "0")
(("1" (REWRITE "value_digit")
(("1"
(REWRITE "expt_x0")
(("1"
(REWRITE "max_significand")
(("1" (ASSERT) NIL)))))))))
("2" (INST + "0")
(("2" (REWRITE "value_digit")
(("2"
(REWRITE "expt_x0")
(("2"
(REWRITE "max_significand")
(("2" (ASSERT) NIL)))))))))))))))))
("2" (ASSERT) NIL)))))
("2" (SPLIT 1)
(("1" (ASSERT) NIL) ("2" (ASSERT) NIL)))))))))))))))
(|min_neg_TCC1| "" (TCC :DEFS !) NIL)
(|min_neg_TCC2| "" (EXPAND "min_fp_neg")
(("" (EXPAND "value")
(("" (EXPAND "neg")
(("" (REWRITE "expt_x1")
(("" (ASSERT)
(("" (LEMMA "expt_pos")
(("" (INST?)
(("" (LEMMA "Sum_pos")
(("" (INST?)
(("" (LEMMA "pos_times_gt")
(("" (INST?)
(("" (GROUND)
(("1" (INST + "p-1")
(("1" (REWRITE "value_digit")
(("1"
(REWRITE "min_significand")
(("1"
(HIDE 1 3 4 5 6)
(("1"
(HIDE -1)
(("1"
(LEMMA "expt_pos")
(("1"
(INST?)
(("1"
(ASSERT)
NIL)))))))))))))))
("2" (HIDE -1 1 3 4 5 6)
(("2" (INST + "p-1")
(("2"
(EXPAND "value_digit")
(("2"
(EXPAND "min_significand")
(("2"
(ASSERT)
(("2"
(LEMMA "expt_pos")
(("2"
(INST?)
(("2"
(ASSERT)
NIL)))))))))))))))))))))))))))))))))))))))
(|max_fp_correct_TCC1| "" (TCC :DEFS !) NIL)
(|max_fp_correct_TCC2| "" (TCC :DEFS !) NIL)
(|max_fp_correct| "" (REWRITE "max_pos")
(("" (REWRITE "max_fp_pos")
(("" (REWRITE "value")
(("" (REWRITE "pos")
(("" (REWRITE "expt_x0")
(("" (ASSERT)
((""
(CASE "forall (i:upto(p)):Sum(i,
(LAMBDA (n: nat):
IF n < p THEN max_significand(n) * (b ^ (-n)) ELSE 0 ENDIF))
* b ^ E_max
= b ^ (1 + E_max) - b ^ (1 + E_max - i)")
(("1" (INST?)
(("1" (EXPAND "value_digit") (("1" (PROPAX) NIL)))))
("2" (HIDE 2)
(("2" (INDUCT "i" 1 "upto_induction[p]")
(("1" (REWRITE "Sum") (("1" (ASSERT) NIL)))
("2" (SKOSIMP*)
(("2" (EXPAND "Sum" +)
(("2" (REPLACE -2)
(("2" (HIDE -2)
(("2" (ASSERT)
(("2"
(REWRITE "max_significand")
(("2"
(LEMMA "expt_plus")
(("2"
(INST-CP - "1" "E_max - jt!1" "b")
(("2"
(INST - "E_max" "-jt!1" "b")
(("2"
(REPLACE -1)
(("2"
(HIDE -1)
(("2"
(REPLACE -1)
(("2"
(HIDE -1)
(("2"
(REWRITE "expt_x1")
(("2"
(ASSERT)
NIL)))))))))))))))))))))))))))))))))))))))))))))))
(|min_fp_correct_TCC1| "" (TCC :DEFS !) NIL)
(|min_fp_correct| "" (EXPAND "min_fp_pos")
(("" (EXPAND "value")
(("" (EXPAND "pos")
(("" (REWRITE "expt_x0")
(("" (ASSERT)
((""
(CASE-REPLACE
"Sum(p,value_digit(min_significand))= b^(1-p)")
(("1" (HIDE -1)
(("1" (LEMMA "expt_plus")
(("1" (INST - "(1 - p)" "E_min" "b")
(("1" (ASSERT) NIL)))))))
("2" (HIDE 2)
(("2" (EXPAND "Sum")
(("2" (EXPAND "value_digit")
(("2" (EXPAND "min_significand")
(("2"
(CASE "forall (i:below(p)):Sum(i,
LAMBDA (n: nat):
IF n < p THEN IF n < p - 1 THEN 0 ELSE 1 ENDIF * b ^ (-n)
ELSE 0
ENDIF)
= 0")
(("1" (INST?) NIL)
("2" (HIDE 2)
(("2" (INDUCT-AND-REWRITE "i" 1 "Sum")
NIL)))))))))))))))))))))))))
(|value0| "" (SKOSIMP*)
(("" (EXPAND "value")
(("" (REWRITE "zero_times3")
(("1" (REWRITE "zero_times3")
(("1" (LEMMA "expt_nonzero")
(("1" (INST? :COPY? T)
(("1" (ASSERT)
(("1" (HIDE -2)
(("1" (INST?)
(("1" (ASSERT)
(("1" (HIDE -1)
(("1" (REWRITE "Sum_zero")
(("1" (PROP)
(("1" (EXPAND "d_zero")
(("1"
(APPLY-EXTENSIONALITY)
(("1"
(EXPAND "value_digit")
(("1"
(INST?)
(("1"
(REWRITE "zero_times3")
(("1"
(LEMMA "expt_nonzero")
(("1"
(INST?)
(("1"
(ASSERT)
NIL)))))))))))))))
("2" (REPLACE -1)
(("2"
(EXPAND "d_zero")
(("2"
(EXPAND "value_digit")
(("2"
(PROPAX)
NIL)))))))))))))))))))))))))))
("2" (ASSERT) NIL)))))))
(|value_of_zero| "" (REWRITE "value0")
(("" (EXPAND "pos_zero") (("" (PROPAX) NIL)))))
(|normal_value| "" (SKOSIMP*)
(("" (CASE-REPLACE "fin!1=finite(sign(fin!1),Exp(fin!1),d(fin!1))")
(("1" (HIDE -1)
(("1"
(CASE "forall (s:sign_rep),(d:digits),(n:upto(E_max-E_min)):
value(finite(s,n+E_min,d))=value(normalize(finite(s,n+E_min,d)))")
(("1" (INST - "sign(fin!1)" "d(fin!1)" "Exp(fin!1)-E_min")
(("1" (ASSERT) NIL) ("2" (ASSERT) NIL)))
("2" (HIDE 2)
(("2" (INDUCT "n" 1 "upto_induction[E_max-E_min]")
(("1" (SKOSIMP*)
(("1" (EXPAND "normalize") (("1" (PROPAX) NIL)))))
("2" (SKOSIMP*)
(("2" (REWRITE "normalize")
(("2" (LIFT-IF)
(("2" (GROUND)
(("2" (INST?)
(("2" (REPLACE -3 :DIR RL)
(("2" (HIDE -3)
(("2" (EXPAND "value")
(("2"
(EXPAND "value_digit")
(("2"
(CASE-REPLACE
"Sum(p,(LAMBDA (n: nat):
IF n < p THEN shift_left(d!1)(n) * (b ^ (-n))
ELSE 0
ENDIF))=b*Sum(p,(LAMBDA (n: nat): IF n < p THEN d!1(n) * (b ^ (-n)) ELSE 0 ENDIF))")
(("1"
(HIDE -1)
(("1"
(LEMMA "expt_plus")
(("1"
(INST - "1" "E_min+jt!1" "b")
(("1"
(REPLACE -1)
(("1"
(HIDE -1)
(("1"
(REWRITE "expt_x1")
(("1"
(ASSERT)
NIL)))))))))))))
("2"
(HIDE 2)
(("2"
(REWRITE "Sum")
(("2"
(ASSERT)
(("2"
(REWRITE "shift_left")
(("2"
(ASSERT)
(("2"
(CASE
"forall (i:below(p)): Sum(i,
(LAMBDA (n: nat):
IF n < p THEN shift_left(d!1)(n) * (b ^ (-n)) ELSE 0 ENDIF))
= b
*
Sum(i+1,
(LAMBDA (n: nat):
IF n < p THEN d!1(n) * (b ^ (-n)) ELSE 0 ENDIF))")
(("1"
(INST?)
(("1" (ASSERT) NIL)))
("2"
(HIDE 2)
(("2"
(INDUCT
"i"
1
"below_induction[p]")
(("1"
(EXPAND "Sum")
(("1"
(EXPAND "Sum")
(("1"
(ASSERT)
NIL)))))
("2"
(SKOSIMP*)
(("2"
(EXPAND "Sum" +)
(("2"
(REPLACE -2)
(("2"
(HIDE -2)
(("2"
(ASSERT)
(("2"
(EXPAND
"shift_left")
(("2"
(LEMMA
"expt_plus")
(("2"
(INST
-
"1"
"-(1+jb!1)"
"b")
(("2"
(REPLACE
-1)
(("2"
(REWRITE
"expt_x1")
(("2"
(ASSERT)
NIL)))))))))))))))))))))))))))))))))))))
("3"
(ASSERT)
NIL)))))))))))))))))))))))))
("3" (REWRITE "fp_num_finite_eta") (("3" (ASSERT) NIL)))))))
("2" (REWRITE "fp_num_finite_eta") NIL)))))
(|value_positive| "" (SKOSIMP*)
(("" (EXPAND "zero?")
(("" (EXPAND "pos")
(("" (GROUND)
(("1" (EXPAND "value")
(("1" (REPLACE -1)
(("1" (REWRITE "expt_x0")
(("1" (ASSERT)
(("1" (LEMMA "pos_times_ge")
(("1" (INST?)
(("1" (LEMMA "expt_pos")
(("1" (INST?)
(("1" (GROUND) NIL)))))))))))))))))
("2" (EXPAND "value")
(("2" (TYPEPRED "sign(fin!1)")
(("2" (ASSERT)
(("2" (REPLACE -1)
(("2" (REWRITE "expt_x1")
(("2" (LEMMA "expt_pos")
(("2" (INST?)
(("2" (ASSERT)
(("2" (LEMMA "Sum_nonneg")
(("2" (INST?)
(("2"
(LEMMA "pos_times_ge")
(("2"
(INST?)
(("2"
(ASSERT)
NIL)))))))))))))))))))))))))))))))))
(|value_negative| "" (ASSERT)
(("" (SKOSIMP*)
(("" (EXPAND "neg")
(("" (EXPAND "zero?")
(("" (EXPAND "value")
(("" (LEMMA "expt_pos")
(("" (INST - "Exp(fin!1)" "b")
(("1" (LEMMA "Sum_nonneg")
(("1" (INST?)
(("1" (LEMMA "pos_times_ge")
(("1" (GROUND)
(("1" (REPLACE -1)
(("1" (REWRITE "expt_x1")
(("1" (ASSERT)
(("1" (INST?) (("1" (ASSERT) NIL)))))))))
("2" (TYPEPRED "sign(fin!1)")
(("2" (ASSERT)
(("2" (REPLACE -1)
(("2"
(REWRITE "expt_x0")
(("2"
(ASSERT)
(("2"
(INST?)
(("2" (ASSERT) NIL)))))))))))))))))
("2" (ASSERT) NIL)))))
("2" (ASSERT)
(("2" (SPLIT)
(("1" (ASSERT) NIL)
("2" (ASSERT) NIL)))))))))))))))))))
(|finite_cover| "" (SKOSIMP*)
(("" (EXPAND "normal?")
(("" (EXPAND "subnormal?")
(("" (GROUND)
(("" (HIDE 2)
((""
(CASE "forall (n:upto(E_max-E_min)),(s:sign_rep),(d:digits):
Exp(normalize(finite(s,n+E_min,d))) = E_min or
d(normalize(finite(s,n+E_min,d)))(0) > 0")
(("1"
(INST - "Exp(fin!1)-E_min" "sign(fin!1)" "d(fin!1)")
(("1" (ASSERT)
(("1" (REWRITE "fp_num_finite_eta")
(("1" (ASSERT) NIL)))))
("2" (ASSERT)
(("2" (HIDE 2 3) (("2" (GROUND) NIL)))))))
("2" (HIDE 2 3)
(("2" (INDUCT "n" 1 "upto_induction[E_max-E_min]")
(("1" (EXPAND "normalize") (("1" (PROPAX) NIL)))
("2" (SKOSIMP*)
(("2" (REWRITE "normalize")
(("2" (LIFT-IF)
(("2" (GROUND)
(("2" (INST?) (("2" (ASSERT) NIL)))))))))))
("3" (SKOSIMP*) (("3" (ASSERT) NIL)))))))
("3" (SKOSIMP*) (("3" (ASSERT) NIL)))))))))))))))
(|finite_disjoint1| "" (SKOSIMP*)
(("" (EXPAND "normal?")
(("" (EXPAND "zero?")
(("" (GROUND)
(("" (REWRITE "normal_value")
(("" (REWRITE "value0")
(("" (REPLACE -2)
(("" (EXPAND "d_zero")
(("" (ASSERT) NIL)))))))))))))))))
(|finite_disjoint2| "" (SKOSIMP*)
(("" (EXPAND "subnormal?") (("" (GROUND) NIL)))))
(|finite_disjoint3| "" (SKOSIMP*)
(("" (EXPAND "subnormal?")
(("" (EXPAND "normal?") (("" (GROUND) NIL)))))))
(|toggle_sign_TCC1| "" (SKOLEM-TYPEPRED) (("" (GROUND) NIL)))
(|toggle_sign_TCC2| "" (SKOLEM-TYPEPRED) (("" (GROUND) NIL)))
(|toggle_finite| "" (TCC :DEFS !) NIL)
(|toggle_infinite| "" (TCC :DEFS !) NIL)
(|toggle_NaN| "" (TCC :DEFS !) NIL)
(|value_toggle_TCC1| "" (TCC :DEFS !) NIL)
(|value_toggle| "" (SKOSIMP*)
(("" (EXPAND "toggle_sign")
(("" (EXPAND "value")
(("" (TYPEPRED "sign(fin!1)")
(("" (GROUND)
(("1" (REPLACE -1)
(("1" (REWRITE "expt_x0")
(("1" (REWRITE "expt_x1") (("1" (ASSERT) NIL)))))))
("2" (REPLACE -1)
(("2" (REWRITE "expt_x1")
(("2" (REWRITE "expt_x0")
(("2" (ASSERT) NIL)))))))))))))))))
(|toggle_d_normalize| "" (SKOSIMP*)
((""
(CASE-REPLACE "fin!1 = finite(sign(fin!1),Exp(fin!1),d(fin!1))")
(("1" (EXPAND "toggle_sign")
(("1"
(CASE "forall (s:sign_rep),(d1:digits),(n:upto(E_max-E_min)):
d(normalize(finite(s,n+E_min,d1))) = d(normalize(finite(1-s,n+E_min,d1)))")
(("1" (INST - "sign(fin!1)" "d(fin!1)" "Exp(fin!1)-E_min")
(("1" (ASSERT) NIL) ("2" (ASSERT) NIL)))
("2" (HIDE -1 2)
(("2" (INDUCT "n" 1 "upto_induction[E_max-E_min]")
(("1" (EXPAND "normalize") (("1" (PROPAX) NIL)))
("2" (SKOSIMP*)
(("2" (EXPAND "normalize" +)
(("2" (LIFT-IF)
(("2" (ASSERT)
(("2" (GROUND) (("2" (INST?) NIL)))))))))))
("3" (SKOLEM-TYPEPRED) (("3" (GROUND) NIL)))))))
("3" (HIDE -1 2)
(("3" (SKOLEM-TYPEPRED) (("3" (GROUND) NIL)))))
("4" (ASSERT) NIL)))))
("2" (REWRITE "fp_num_finite_eta") NIL)))))
(|toggle_Exp_normalize| "" (SKOSIMP*)
((""
(CASE-REPLACE "fin!1 = finite(sign(fin!1),Exp(fin!1),d(fin!1))")
(("1" (EXPAND "toggle_sign")
(("1"
(CASE "forall (s:sign_rep),(d1:digits),(n:upto(E_max-E_min)):
Exp(normalize(finite(s,n+E_min,d1))) = Exp(normalize(finite(1-s,n+E_min,d1)))")
(("1" (INST - "sign(fin!1)" "d(fin!1)" "Exp(fin!1)-E_min")
(("1" (ASSERT) NIL) ("2" (ASSERT) NIL)))
("2" (HIDE -1 2)
(("2" (INDUCT "n" 1 "upto_induction[E_max-E_min]")
(("1" (EXPAND "normalize") (("1" (PROPAX) NIL)))
("2" (SKOSIMP*)
(("2" (EXPAND "normalize" +)
(("2" (LIFT-IF)
(("2" (ASSERT)
(("2" (GROUND) (("2" (INST?) NIL)))))))))))
("3" (SKOLEM-TYPEPRED) (("3" (GROUND) NIL)))))))
("3" (HIDE -1 2)
(("3" (SKOLEM-TYPEPRED) (("3" (GROUND) NIL)))))
("4" (ASSERT) NIL)))))
("2" (REWRITE "fp_num_finite_eta") NIL)))))
(|toggle_zero?| "" (SKOSIMP*)
(("" (EXPAND "zero?")
(("" (REWRITE "toggle_finite")
(("" (REWRITE "value_toggle") (("" (GROUND) NIL)))))))))
(|toggle_normal?| "" (SKOSIMP*)
(("" (EXPAND "normal?")
(("" (REWRITE "toggle_d_normalize")
(("" (REWRITE "toggle_finite") (("" (ASSERT) NIL)))))))))
(|toggle_subnormal?| "" (SKOSIMP*)
(("" (EXPAND "subnormal?")
(("" (REWRITE "toggle_d_normalize")
(("" (REWRITE "toggle_Exp_normalize")
(("" (REWRITE "toggle_zero?")
(("" (REWRITE "toggle_finite")
(("" (ASSERT) NIL)))))))))))))
(|value_digit_le_TCC1| "" (TCC :DEFS !) NIL)
(|value_digit_le| "" (SKOSIMP*)
(("" (REWRITE "value_digit")
(("" (LIFT-IF)
(("" (SPLIT)
(("1" (FLATTEN)
(("1" (REWRITE "both_sides_times_pos_le1")
(("1" (ASSERT) NIL)
("2" (LEMMA "expt_pos")
(("2" (INST?) (("2" (ASSERT) NIL)))))))))
("2" (FLATTEN)
(("2" (LEMMA "expt_pos")
(("2" (INST?)
(("1" (REWRITE "pos_times_le") (("1" (ASSERT) NIL)))
("2" (ASSERT) NIL)))))))))))))))
(|Sum_d_lt_b| "" (INDUCT "j")
(("1" (EXPAND "Sum")
(("1" (EXPAND "Sum")
(("1" (EXPAND "value_digit")
(("1" (REWRITE "expt_x0")
(("1" (SKOSIMP*)
(("1" (LIFT-IF) (("1" (GROUND) NIL)))))))))))))
("2" (SKOSIMP*)
(("2" (REWRITE "Sum")
(("2" (INST?)
(("2" (LEMMA "value_digit_le")
(("2" (INST?)
(("2" (ASSERT)
(("2" (CASE-REPLACE "b ^ (-(1 + j!1)) * b = b^(-j!1)")
(("1" (HIDE -1) (("1" (ASSERT) NIL)))
("2" (HIDE -1 -2 2)
(("2" (LEMMA "expt_plus")
(("2" (INST - "-(1+j!1)" "1" "b")
(("2" (REWRITE "expt_x1")
(("2" (ASSERT) NIL)))))))))))))))))))))))
("3" (SKOSIMP*) (("3" (ASSERT) NIL)))))
(|Sum_d_lt1_TCC1| "" (TCC :DEFS !) NIL)
(|Sum_d_lt1_TCC2| "" (TCC :DEFS !) NIL)
(|Sum_d_lt1| "" (INDUCT "j")
(("1" (EXPAND "Sum")
(("1" (EXPAND "Sum")
(("1" (EXPAND "value_digit")
(("1" (REWRITE "expt_x0")
(("1" (LIFT-IF)
(("1" (ASSERT)
(("1" (GROUND)
(("1" (SKOSIMP*) (("1" (ASSERT) NIL)))))))))))))))))
("2" (SKOSIMP*)
(("2" (REWRITE "Sum")
(("2" (INST?)
(("2" (ASSERT)
(("2" (LEMMA "value_digit_le")
(("2" (INST?)
(("2" (ASSERT)
(("2"
(CASE-REPLACE "b ^ (-(1 + j!1)) * b = b^(-j!1)")
(("1" (ASSERT) NIL)
("2" (HIDE -1 -2 -3 2)
(("2" (LEMMA "expt_plus")
(("2" (INST - "-(1+j!1)" "1" "b")
(("2" (REWRITE "expt_x1")
(("2" (ASSERT) NIL)))))))))))))))))))))))))
("3" (SKOSIMP*) (("3" (ASSERT) NIL))) ("4" (ASSERT) NIL)))
(|Sum_d_ge1| "" (INDUCT "j")
(("1" (EXPAND "Sum")
(("1" (SKOSIMP*)
(("1" (REWRITE "value_digit")
(("1" (LIFT-IF)
(("1" (ASSERT)
(("1" (REWRITE "expt_x0")
(("1" (ASSERT)
(("1" (LEMMA "Sum_nonneg")
(("1" (INST?) (("1" (ASSERT) NIL)))))))))))))))))))
("2" (SKOSIMP*)
(("2" (REWRITE "Sum") (("2" (INST?) (("2" (ASSERT) NIL)))))))
("3" (ASSERT) NIL)))
(|value_sig_lt_b| "" (SKOSIMP*)
(("" (LEMMA "Sum_d_lt_b")
(("" (INST - "d!1" "p-1")
(("1" (ASSERT)
(("1" (LEMMA "expt_pos")
(("1" (INST?) (("1" (ASSERT) NIL)))))))
("2" (ASSERT) NIL)))))))
(|value_sig_lt1| "" (SKOSIMP*)
(("" (LEMMA "Sum_d_lt1")
(("" (INST - "d!1" "p-1")
(("1" (LEMMA "expt_pos")
(("1" (INST?) (("1" (ASSERT) NIL) ("2" (ASSERT) NIL)))))
("2" (ASSERT) NIL)))))))
(|value_sig_ge1| "" (SKOSIMP*)
(("" (LEMMA "Sum_d_ge1")
(("" (INST - "d!1" "p-1")
(("1" (ASSERT) NIL) ("2" (ASSERT) NIL)))))))
(|abs_value_fin| "" (SKOSIMP*)
(("" (EXPAND "value")
((""
(CASE "b ^ (Exp(fin!1)) * Sum(p, value_digit(d(fin!1))) >=0")
(("1" (TYPEPRED "sign(fin!1)")
(("1" (PROP)
(("1" (REPLACE -1)
(("1" (REWRITE "expt_x0")
(("1" (EXPAND "abs") (("1" (ASSERT) NIL)))))))
("2" (REPLACE -1)
(("2" (REWRITE "expt_x1")
(("2" (EXPAND "abs")
(("2" (ASSERT)
(("2" (LIFT-IF) (("2" (GROUND) NIL)))))))))))))))
("2" (HIDE 2)
(("2" (LEMMA "expt_pos")
(("2" (INST?)
(("1" (LEMMA "Sum_nonneg")
(("1" (INST?)
(("1" (REWRITE "pos_times_ge") (("1" (ASSERT) NIL)))
("2" (ASSERT) NIL)))))
("2" (ASSERT) NIL)))))))
("3" (ASSERT) NIL) ("4" (ASSERT) NIL)))))))
(|min_significand_min| "" (SKOSIMP*)
(("" (EXPAND "Sum" + 1)
(("" (GROUND)
(("" (LIFT-IF)
(("" (GROUND)
(("" (REWRITE "value_digit")
(("" (REWRITE "min_significand")
(("" (ASSERT)
((""
(CASE-REPLACE
"Sum(p - 1, value_digit(min_significand))=0")
(("1" (HIDE -1)
(("1" (ASSERT)
(("1" (LEMMA "Sum_pos")
(("1" (INST?)
(("1" (GROUND)
(("1"
(SKOSIMP*)
(("1"
(LEMMA "Sum_ge")
(("1"
(INST?)
(("1"
(INST - "value_digit(d!1)(i!1)")
(("1"
(GROUND)
(("1"
(REWRITE "value_digit")
(("1"
(TYPEPRED "i!1")
(("1"
(CASE
"d!1(i!1) * b ^ (-i!1) >= b ^ (-(p - 1))")
(("1" (ASSERT) NIL)
("2"
(LEMMA
"ge_times_ge_pos")
(("2"
(INST
-
"b ^ (-(p - 1))"
"1"
"d!1(i!1)"
"b ^ (-i!1)")
(("2"
(GROUND)
(("2"
(HIDE
-3
-4
-5
2
3
4
5)
(("2"
(LEMMA
"both_sides_expt_gt1_le")
(("2"
(INST
-
"b"
"-(p-1)"
"-i!1")
(("2"
(ASSERT)
NIL)))))))))))))))))))
("2"
(INST?)
(("2"
(ASSERT)
NIL)))))))))))))
("2"
(CASE "d!1=d_zero")
(("1" (PROPAX) NIL)
("2"
(APPLY-EXTENSIONALITY)
(("2"
(EXPAND "d_zero")
(("2"
(INST?)
(("2"
(HIDE 2 4 5 6 7)
(("2"
(EXPAND "value_digit")
(("2"
(REWRITE "pos_times_gt")
(("2"
(LEMMA "expt_pos")
(("2"
(INST?)
(("2"
(ASSERT)
NIL)))))))))))))))))))))))))))))
("2" (HIDE 2 3 4)
(("2"
(CASE "forall (i:below(p)): Sum(i,value_digit(min_significand)) = 0")
(("1" (INST?) NIL)
("2" (HIDE 2)
(("2" (INDUCT "i" 1 "below_induction[p]")
(("1" (EXPAND "Sum") (("1" (PROPAX) NIL)))
("2" (SKOSIMP*)
(("2"
(REWRITE "Sum" +)
(("2"
(REWRITE "value_digit")
(("2"
(REWRITE "min_significand")
(("2"
(GROUND)
NIL)))))))))))))))))))))))))))))))))))
(|sign_normal| "" (SKOSIMP*)
((""
(CASE "forall (s:sign_rep),(d:digits),(n:upto(E_max-E_min)):
s=sign(normalize(finite(s,n+E_min,d)))")
(("1"
(CASE-REPLACE
"fin!1 = finite(sign(fin!1),Exp(fin!1),d(fin!1))")
(("1" (ASSERT)
(("1" (INST - "sign(fin!1)" "d(fin!1)" "Exp(fin!1)-E_min")
(("1" (ASSERT) NIL)))))
("2" (ASSERT) (("2" (REWRITE "fp_num_finite_eta") NIL)))))
("2" (HIDE 2)
(("2" (INDUCT "n" 1 "upto_induction[E_max-E_min]")
(("1" (SKOSIMP*)
(("1" (EXPAND "normalize") (("1" (PROPAX) NIL)))))
("2" (SKOSIMP*)
(("2" (REWRITE "normalize")
(("2" (LIFT-IF)
(("2" (GROUND) (("2" (INST?) NIL)))))))))))))
("3" (ASSERT) NIL)))))
(|value_normal_TCC1| "" (TCC :DEFS !) NIL)
(|value_normal| "" (SKOSIMP*)
(("" (REWRITE "normal_value")
(("" (REWRITE "abs_value_fin")
(("" (EXPAND "normal?")
(("" (ASSERT)
(("" (EXPAND "max_pos")
(("" (EXPAND "value")
(("" (EXPAND "max_fp_pos")
(("" (EXPAND "pos")
(("" (REWRITE "expt_x0")
(("" (ASSERT)
(("" (PROP)
(("1" (LEMMA "value_sig_ge1")
(("1" (INST?)
(("1"
(ASSERT)
(("1"
(LEMMA "both_sides_expt_gt1_le")
(("1"
(INST
-
"b"
"E_min"
"(Exp(normalize(fin!1)))")
(("1"
(ASSERT)
(("1"
(LEMMA "le_times_le_pos")
(("1"
(INST
-
"b^E_min"
"1"
"Sum(p, value_digit(d(normalize(fin!1))))"
"b ^ (Exp(normalize(fin!1)))")
(("1" (ASSERT) NIL)
("2"
(LEMMA "expt_pos")
(("2"
(INST?)
(("2"
(ASSERT)
NIL)))))))))))))))))))))
("2" (LEMMA "both_sides_expt_gt1_le")
(("2"
(INST - "b" "(Exp(normalize(fin!1)))"
"E_max")
(("2"
(ASSERT)
(("2"
(LEMMA "le_times_le_pos")
(("2"
(INST
-
"b ^ (Exp(normalize(fin!1)))"
"Sum(p, value_digit(d(normalize(fin!1))))"
"Sum(p, value_digit(max_significand))"
" b ^ E_max")
(("1"
(ASSERT)
(("1"
(HIDE -1 2)
(("1"
(REWRITE "Sum_le")
(("1"
(HIDE -1 2)
(("1"
(SKOSIMP*)
(("1"
(EXPAND "value_digit")
(("1"
(LEMMA "expt_pos")
(("1"
(INST?)
(("1"
(REWRITE
"both_sides_times_pos_le1")
(("1"
(EXPAND
"max_significand")
(("1"
(ASSERT)
NIL)))))))))))))))))))))
("2"
(LEMMA "expt_pos")
(("2"
(INST?)
(("2"
(ASSERT)
NIL)))))))))))))))))))))))))))))))))))))))
(|value_subnormal_TCC1| "" (TCC :DEFS !) NIL)
(|value_subnormal| "" (SKOSIMP*)
(("" (REWRITE "normal_value")
(("" (REWRITE "abs_value_fin")
(("" (EXPAND "min_pos")
(("" (EXPAND "value")
(("" (EXPAND "min_fp_pos")
(("" (EXPAND "pos")
(("" (REWRITE "expt_x0")
(("" (ASSERT)
(("" (EXPAND "subnormal?")
(("" (ASSERT)
(("" (GROUND)
(("1" (EXPAND "zero?")
(("1" (LEMMA "both_sides_times_pos_le1")
(("1"
(INST
-
"b ^ (Exp(normalize(fin!1)))"
"Sum(p, value_digit(min_significand))"
"Sum(p, value_digit(d(normalize(fin!1))))")
(("1"
(GROUND)
(("1"
(HIDE 2 3)
(("1"
(REWRITE "normal_value")
(("1"
(REWRITE "value0")
(("1"
(REWRITE
"min_significand_min")
NIL)))))))))
("2"
(LEMMA "expt_pos")
(("2"
(INST?)
(("2" (ASSERT) NIL)))))))))))
("2" (LEMMA "value_sig_lt1")
(("2" (INST?)
(("2"
(ASSERT)
(("2"
(ASSERT)
(("2"
(LEMMA "expt_pos")
(("2"
(INST?)
(("2"
(LEMMA
"both_sides_times_pos_lt1")
(("2"
(INST
-
"b ^ (Exp(normalize(fin!1)))"
"Sum(p, value_digit(d(normalize(fin!1))))"
"1")
(("1" (ASSERT) NIL)
("2"
(ASSERT)
NIL)))))))))))))))))))))))))))))))))))))))))
(|value_nonzero| "" (SKOSIMP*)
(("" (LEMMA "value_normal")
(("" (INST?)
(("" (LEMMA "value_subnormal")
(("" (INST?)
(("" (LEMMA "finite_cover")
(("" (INST?)
(("" (GROUND)
(("1" (EXPAND "min_pos")
(("1" (REWRITE "min_fp_correct")
(("1" (LEMMA "both_sides_expt_gt1_le")
(("1" (INST - "b" "(1 + E_min - p)" "E_min")
(("1" (GROUND) NIL)))))))))
("2" (LEMMA "both_sides_expt_gt1_le")
(("2" (REWRITE "max_fp_correct")
(("2" (INST - "b" "E_min" "E_max")
(("2" (GROUND)
(("2"
(CASE "b^E_max < b ^ (1 + E_max) - b ^ (1 + E_max - p)")
(("1" (GROUND) NIL)
("2" (HIDE -1 -2 -3 -4 -5 2 3 4)
(("2"
(LEMMA "exponent_adjust")
(("2"
(INST - "b" "E_max" "p-1")
(("2"
(ASSERT)
NIL)))))))))))))))))))))))))))))))))
(|scale_value_TCC1| "" (TCC)
(("1" (REWRITE "pos_times_ge")
(("1" (ASSERT)
(("1" (LEMMA "expt_pos")
(("1" (EXPAND "^")
(("1" (INST?) (("1" (ASSERT) NIL)))))))))))
("2" (LEMMA "expt_pos")
(("2" (EXPAND "^")
(("2" (INST?)
(("2" (ASSERT)
(("2" (LEMMA "expt_pos")
(("2" (ASSERT)
(("2" (INST -1 "-n!1" "b")
(("2" (ASSERT)
(("2" (LEMMA "pos_times_gt")
(("2"
(INST -1 "d!1(n!1)"
"expt(b, m!1) * (1 / (b * expt(b, -(-n!1) - 1)))")
(("1" (ASSERT)
(("1" (PROP)
(("1" (LEMMA "pos_times_gt")
(("1"
(INST
-1
"expt(b, m!1)"
"(1 / (b * expt(b, -(-n!1) - 1)))")
(("1" (ASSERT) NIL)
("2"
(LEMMA "zero_times3")
(("2"
(INST?)
(("2"
(ASSERT)
(("2"
(LEMMA "expt_nonzero_aux")
(("2"
(INST?)
(("2"
(ASSERT)
NIL)))))))))))))))))))
("2" (LEMMA "zero_times3")
(("2" (INST?)
(("2" (ASSERT)
(("2"
(LEMMA "zero_times3")
(("2"
(INST?)
(("2"
(ASSERT)
(("2"
(LEMMA "expt_nonzero_aux")
(("2"
(INST?)
(("2"
(ASSERT)
NIL)))))))))))))))))))))))))))))))))))))))
(|scaled_Sum_int| "" (SKOLEM!)
(("" (INDUCT "m" 1 "upto_induction[n!1+1]")
(("1" (REWRITE "Sum")
(("1" (EXPAND "integer?") (("1" (PROPAX) NIL)))))
("2" (SKOSIMP*)
(("2" (REWRITE "Sum" +)
(("2" (REWRITE "scale_value")
(("2" (REWRITE "value_digit")
(("2" (LIFT-IF)
(("2" (GROUND)
(("2" (CASE "FORALL (i,j:int): integer?(i+j)")
(("1" (INST?)
(("1" (HIDE -3 2)
(("1" (REWRITE "associative_mult" :DIR RL)
(("1" (REWRITE "expt_plus" :DIR RL)
(("1"
(CASE "FORALL (i,j:int): integer?(i*j)")
(("1"
(INST?)
(("1" (ASSERT) NIL)
("2"
(ASSERT)
(("2"
(HIDE 2)
(("2"
(CASE
"forall (n:nat): integer?(b^n)")
(("1"
(INST?)
(("1"
(EXPAND "integer?")
(("1" (PROPAX) NIL)))))
("2"
(SKOSIMP*)
(("2"
(EXPAND "integer?")
(("2"
(PROPAX)
NIL)))))))))))))
("2"
(EXPAND "integer?")
(("2" (PROPAX) NIL)))))))))))
("2" (EXPAND "integer?") (("2" (PROPAX) NIL)))))
("2" (EXPAND "integer?" 1)
(("2" (PROPAX) NIL)))))))))))))))))))))
(|scale_value_p_TCC1| "" (TCC :DEFS !) NIL)
(|scale_value_p_TCC2| "" (SKOSIMP*)
(("" (CASE "integer?(scale_value(d!1, p - 1)(n!1))")
(("1" (EXPAND "integer?") (("1" (ASSERT) NIL)))
("2" (HIDE 2)
(("2" (REWRITE "scale_value")
(("2" (REWRITE "value_digit")
(("2" (LIFT-IF)
(("2" (GROUND)
(("1"
(CASE-REPLACE
"(d!1(n!1) * b ^ (p - 1) * b ^ (-n!1))=(d!1(n!1) * b ^ (p - 1 - n!1))")
(("1" (HIDE -1)
(("1" (CASE "FORALL (i,j:int): integer?(i*j)")
(("1" (INST?)
(("1" (ASSERT)
(("1" (HIDE 2)
(("1" (EXPAND "^")
(("1"
(ASSERT)
(("1"
(CASE
"FORALL (n:nat): integer_pred(expt(b, n))")
(("1" (INST?) NIL)
("2"
(HIDE -1 2)
(("2"
(INDUCT "n")
(("2"
(SKOSIMP*)
NIL)))))))))))))))))
("2" (EXPAND "integer?")
(("2" (PROPAX) NIL)))))))
("2" (LEMMA "expt_plus")
(("2" (INST?)
(("2" (INST -1 "-n!1")
(("2" (ASSERT) NIL)))))))))
("2" (EXPAND "integer?")
(("2" (PROPAX) NIL)))))))))))))
("3" (ASSERT) NIL)))))
(|scaled_Sum_i| "" (INDUCT "n")
(("1" (EXPAND "Sum") (("1" (PROPAX) NIL)))
("2" (SKOSIMP*)
(("2" (EXPAND "Sum" +)
(("2" (INST?)
(("2" (REWRITE "scale_value") (("2" (ASSERT) NIL)))))))))))
(|scaled_Sum| "" (SKOSIMP*)
(("" (REWRITE "scaled_Sum_i")
(("" (REWRITE "scale_value_p")
(("" (REPLACE-ETA "scale_value(d!1, (p - 1))") NIL)))))))
(|floor_Sum| "" (SKOSIMP*)
(("" (REWRITE "scaled_Sum_i")
(("" (LEMMA "Sum_split")
(("" (INST - "scale_value(d!1, i!1)" "p" "i!1+1")
(("" (REPLACE -1)
(("" (HIDE -1)
(("" (LEMMA "floor_plus_int")
((""
(INST - "Sum(i!1 + 1, scale_value(d!1, i!1))"
"Sum(p - (i!1 + 1),
LAMBDA (k: nat):
scale_value(d!1, i!1)(k + (i!1 + 1)))")
(("1" (REPLACE -1)
(("1" (HIDE -1)
(("1" (ASSERT)
(("1" (LEMMA "floor_Sum_mant")
(("1" (INST?)
(("1" (HIDE 2)
(("1"
(SKOSIMP*)
(("1"
(REWRITE "scale_value")
(("1"
(REWRITE "value_digit")
(("1"
(LIFT-IF)
(("1"
(GROUND)
(("1"
(LEMMA "expt_plus")
(("1"
(INST
-
"(-(1 + i!1 + i!2))"
"i!1"
"b")
(("1"
(LEMMA
"both_sides_times_pos_le1")
(("1"
(INST
-
"b ^ (-i!2 - 1)"
"d!1(1 + i!1 + i!2)"
"(b-1)")
(("1" (ASSERT) NIL)
("2"
(HIDE -1 -2 2)
(("2"
(LEMMA "expt_pos")
(("2"
(INST?)
(("2"
(ASSERT)
NIL)))))))))))))))
("2"
(LEMMA "pos_times_le")
(("2"
(INST
-
"(b-1)"
"b ^ (-i!2 - 1)")
(("2"
(LEMMA "expt_pos")
(("2"
(INST?)
(("2"
(ASSERT)
NIL)))))))))))))))))))))))))))))))
("2" (HIDE 2)
(("2" (LEMMA "scaled_Sum_int")
(("2" (EXPAND "integer?")
(("2" (INST?) NIL)))))))))))))))))))))))
(|mod_Sum_TCC1| "" (SKOSIMP*)
(("" (LEMMA "scaled_Sum_int")
(("" (EXPAND "integer?") (("" (INST?) NIL)))))))
(|mod_Sum_TCC2| "" (ASSERT) NIL)
(|mod_Sum| "" (SKOSIMP*)
(("" (REWRITE "Sum")
(("" (REWRITE "scale_value")
(("" (REWRITE "value_digit")
((""
(CASE-REPLACE
"(d!1(i!1) * b ^ (-i!1) * b ^ i!1) = d!1(i!1) * (b ^ (-i!1) * b ^ i!1)")
(("1" (HIDE -1)
(("1" (LEMMA "expt_plus")
(("1" (INST?)
(("1" (REPLACE -1 :DIR RL)
(("1" (HIDE -1)
(("1" (REWRITE "expt_x0")
(("1" (ASSERT)
(("1" (LEMMA "mod_of_mod")
(("1" (INST?)
(("1"
(REPLACE -1 :DIR RL)
(("1"
(HIDE -1)
(("1"
(CASE-REPLACE
"mod(Sum(i!1, scale_value(d!1, i!1)),b) = 0")
(("1"
(HIDE -1)
(("1"
(REWRITE "mod_lt_nat")
NIL)))
("2"
(HIDE 2)
(("2"
(CASE
"forall (j:upto(i!1)): mod(Sum(j,scale_value(d!1,i!1)),b) = 0")
(("1" (INST?) NIL)
("2"
(HIDE 2)
(("2"
(INDUCT
"j"
1
"upto_induction[i!1]")
(("1"
(EXPAND "Sum")
(("1"
(REWRITE "mod_zero")
NIL)))
("2"
(SKOSIMP*)
(("2"
(EXPAND "Sum" +)
(("2"
(REWRITE
"scale_value")
(("2"
(REWRITE
"value_digit")
(("2"
(CASE-REPLACE
"d!1(jt!1) * b ^ (-jt!1) * b ^ i!1 = d!1(jt!1) * (b ^ (-jt!1) * b ^ i!1)")
(("1"
(HIDE -1)
(("1"
(LEMMA
"expt_plus")
(("1"
(INST?)
(("1"
(REPLACE
-1
:DIR
RL)
(("1"
(HIDE
-1)
(("1"
(LEMMA
"mod_of_mod")
(("1"
(INST?)
(("1"
(REPLACE
-1
:DIR
RL)
(("1"
(HIDE
-1)
(("1"
(REPLACE
-2)
(("1"
(HIDE
-2)
(("1"
(CASE-REPLACE
"d!1(jt!1) * b ^ ((-jt!1) + i!1) = (d!1(jt!1) * b ^ ((-jt!1) + i!1-1))*b")
(("1"
(HIDE
-1)
(("1"
(LEMMA
"mod_sum")
(("1"
(INST
-
"0"
"b"
"_")
(("1"
(REWRITE
"mod_zero")
(("1"
(INST?)
(("1"
(ASSERT)
NIL)
("2"
(REWRITE
"closed_times")
(("2"
(CASE
"forall (n:nat):integer_pred(b^n)")
(("1"
(INST?)
NIL)
("2"
(SKOSIMP*)
(("2"
(ASSERT)
NIL)))))))))))))))))
("2"
(HIDE
2)
(("2"
(CASE
"b ^ ((-jt!1) + i!1 - 1) * b = b^(i!1-jt!1)")
(("1"
(ASSERT)
NIL)
("2"
(HIDE
2)
(("2"
(LEMMA
"expt_plus")
(("2"
(INST
-
"i!1-jt!1"
"(-1)"
"b")
(("2"
(REPLACE
-1)
(("2"
(REWRITE
"expt_inverse")
(("2"
(REWRITE
"expt_x1")
(("2"
(ASSERT)
NIL)))))))))))))))))))))))))))
("2"
(LEMMA
"scaled_Sum_int")
(("2"
(INST?)
(("2"
(ASSERT)
(("2"
(EXPAND
"integer?")
(("2"
(PROPAX)
NIL)))))))))
("3"
(HIDE
-2
2)
(("3"
(REWRITE
"closed_times")
(("3"
(CASE
"forall (n:nat):integer_pred(b^n)")
(("1"
(INST?)
NIL)
("2"
(SKOSIMP*)
(("2"
(ASSERT)
NIL)))))))))))))))))))))))
("2"
(ASSERT)
NIL)))))))))))
("3"
(LEMMA "scaled_Sum_int")
(("3"
(INST?)
(("3"
(EXPAND "integer?")
(("3"
(ASSERT)
NIL)))))))
("4"
(LEMMA "scaled_Sum_int")
(("4"
(INST?)
(("4"
(EXPAND "integer?")
(("4"
(ASSERT)
NIL)))))))))))
("3"
(SKOSIMP*)
(("3"
(LEMMA "scaled_Sum_int")
(("3"
(INST?)
(("3"
(ASSERT)
(("3"
(EXPAND "integer?")
(("3"
(PROPAX)
NIL)))))))))))))))
("3"
(LEMMA "scaled_Sum_int")
(("3"
(INST?)
(("3"
(ASSERT)
(("3"
(EXPAND "integer?")
(("3"
(PROPAX)
NIL)))))))))))))))
("2"
(LEMMA "scaled_Sum_int")
(("2"
(INST?)
(("2"
(ASSERT)
(("2"
(EXPAND "integer?")
(("2"
(PROPAX)
NIL)))))))))))))))))))))))))))
("2" (ASSERT) NIL))))))))))))
$$$sum_hack.pvs
sum_hack % [ parameters ]
: THEORY
BEGIN
% ASSUMING
% assuming declarations
% ENDASSUMING
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Some stuff that will eventually be loaded from a library,
% once the PVS library mechanism works.
i,j,k:var nat
F: var [nat->real]
Sum(j,F):recursive real =
if j=0 then 0 else F(j-1)+Sum(j-1,F) endif
measure j
F1,F2: var [nat->nonneg_real]
Sum_nonneg: lemma Sum(j,F1)>=0
JUDGEMENT Sum HAS_TYPE [nat,[nat->nonneg_real]->nonneg_real]
Sum_zero: lemma Sum(j,F1)=0 iff forall (i:below(j)): F1(i)=0
Sum_pos: lemma Sum(j,F1)>0 iff (exists (i:below(j)): F1(i)>0)
Sum_le: lemma (forall (i:below(j)): F1(i) <= F2(i)) => Sum(j,F1)<=Sum(j,F2)
Sum_ge1: lemma (exists (i:below(j)): F1(i)>=1) => Sum(j,F1)>=1
pz: var posreal
Sum_ge: lemma (exists (i:below(j)): F1(i)>= pz) => Sum(j,F1)>=pz
Sum_split: lemma forall (i:upto(j)):
Sum(j,F) = Sum(i,F) + Sum(j-i,lambda k: F(k+i))
END sum_hack
$$$sum_hack.prf
(|sum_hack| (|Sum_TCC1| "" (TCC :DEFS !) NIL)
(|Sum_TCC2| "" (TCC :DEFS !) NIL)
(|Sum_nonneg| "" (INDUCT-AND-REWRITE "j" 1 "Sum") NIL)
(|Sum_TCC3| "" (SKOSIMP*) (("" (REWRITE "Sum_nonneg") NIL)))
(|Sum_zero| "" (INDUCT "j")
(("1" (EXPAND "Sum") (("1" (ASSERT) (("1" (SKOSIMP*) NIL)))))
("2" (SKOSIMP*)
(("2" (REWRITE "Sum")
(("2" (INST?)
(("2" (PROP)
(("1" (SKOSIMP*) (("1" (INST?) (("1" (ASSERT) NIL)))))
("2" (INST?) (("2" (ASSERT) NIL)))
("3" (TYPEPRED "Sum(j!1,F1!1)")
(("3" (TYPEPRED "F1!1(j!1)") (("3" (ASSERT) NIL)))))
("4" (SKOSIMP*) (("4" (INST?) NIL)))))))))))))
(|Sum_pos| "" (INDUCT "j")
(("1" (EXPAND "Sum")
(("1" (SKOSIMP*) (("1" (GROUND) (("1" (SKOSIMP*) NIL)))))))
("2" (SKOSIMP*)
(("2" (REWRITE "Sum")
(("2" (INST?)
(("2" (LEMMA "Sum_nonneg")
(("2" (INST?)
(("2" (PROP)
(("1" (SKOSIMP*) (("1" (INST?) NIL)))
("2" (ASSERT) NIL)
("3" (INST + "j!1") (("3" (ASSERT) NIL)))
("4" (SKOSIMP*)
(("4" (INST?) (("4" (ASSERT) NIL)))))))))))))))))))
(|Sum_le| "" (INDUCT "j")
(("1" (EXPAND "Sum") (("1" (PROPAX) NIL)))
("2" (SKOSIMP*)
(("2" (EXPAND "Sum" +)
(("2" (INST - "F1!1 " "F2!1")
(("2" (PROP)
(("1" (INST?) (("1" (ASSERT) NIL)))
("2" (SKOSIMP*) (("2" (INST?) NIL)))))))))))))
(|Sum_ge1| "" (INDUCT "j")
(("1" (SKOSIMP*) NIL)
("2" (SKOSIMP*)
(("2" (REWRITE "Sum")
(("2" (INST?)
(("2" (ASSERT)
(("2" (LEMMA "Sum_nonneg")
(("2" (INST?)
(("2" (INST?) (("2" (ASSERT) NIL)))))))))))))))))
(|Sum_ge| "" (INDUCT "j")
(("1" (SKOSIMP*) NIL)
("2" (SKOSIMP*)
(("2" (REWRITE "Sum")
(("2" (INST - "F1!1" "pz!1")
(("2" (PROP)
(("1" (ASSERT) NIL)
("2" (INST?)
(("2" (ASSERT)
(("2" (GROUND)
(("2" (LEMMA "Sum_nonneg")
(("2" (INST?)
(("2" (ASSERT) NIL)))))))))))))))))))))
(|Sum_split_TCC1| "" (TCC) NIL)
(|Sum_split| "" (INDUCT "j")
(("1" (SKOSIMP*) (("1" (EXPAND "Sum") (("1" (PROPAX) NIL)))))
("2" (SKOSIMP*)
(("2" (TYPEPRED "i!1")
(("2" (EXPAND "Sum" + (1 3))
(("2" (LIFT-IF)
(("2" (GROUND)
(("1" (EXPAND "Sum" + 2) (("1" (PROPAX) NIL)))
("2" (INST - "F!1" "i!1")
(("2" (ASSERT) NIL))))))))))))))))
$$$sum_lemmas.pvs
sum_lemmas [b:above(1)]: THEORY
BEGIN
importing sum_hack
i: var nat
F1: var [nat->nonneg_real]
mant_digit_fun: type = {F1| forall i: F1(i)<=(b-1)*b^(-i-1)}
d: var mant_digit_fun
Sum_pos_less_1: lemma
0<=Sum(i,d) & Sum(i,d)<= 1-b^(-i)
floor_Sum_mant: lemma
floor(Sum(i,d))=0
END sum_lemmas
$$$sum_lemmas.prf
(|sum_lemmas| (|mant_digit_fun_TCC1| "" (TCC) NIL)
(|Sum_pos_less_1_TCC1| "" (TCC) NIL)
(|Sum_pos_less_1| "" (INDUCT "i")
(("1" (EXPAND "Sum")
(("1" (REWRITE "expt_x0") (("1" (ASSERT) NIL)))))
("2" (SKOSIMP*)
(("2" (REWRITE "Sum")
(("2" (INST?)
(("2" (ASSERT)
(("2" (TYPEPRED "d!1")
(("2" (INST?)
(("2" (ASSERT)
(("2" (CASE-REPLACE "b ^ (-j!1 - 1) * b = b^(-j!1)")
(("1" (ASSERT) NIL)
("2" (HIDE -1 -2 2)
(("2" (LEMMA "expt_plus")
(("2" (INST - "(-(j!1+1))" "1" "b")
(("2" (REWRITE "expt_x1")
(("2" (ASSERT) NIL)))))))))))))))))))))))))
("3" (HIDE 2) (("3" (SKOSIMP*) (("3" (ASSERT) NIL)))))
("4" (SKOSIMP*) (("4" (ASSERT) NIL)))))
(|floor_Sum_mant| "" (SKOSIMP*)
(("" (LEMMA "Sum_pos_less_1")
(("" (INST?)
(("" (LEMMA "expt_pos")
(("" (INST?)
(("1" (CASE "1-b^(-i!1)<1")
(("1" (CASE "Sum(i!1, d!1) < 1")
(("1" (FLATTEN)
(("1" (HIDE -2 -3 -5)
(("1" (ASSERT)
(("1"
(CASE "forall (r:real): floor(r)=0 iff 0<=r & r<1")
(("1" (INST?) (("1" (ASSERT) NIL)))
("2" (HIDE -1 -2 2) (("2" (TCC) NIL)))))))))))
("2" (ASSERT) NIL)))
("2" (ASSERT) NIL) ("3" (ASSERT) NIL)))
("2" (SPLIT)
(("1" (ASSERT) NIL) ("2" (ASSERT) NIL))))))))))))))
$$$enumerated_type_defs.pvs
enumerated_type_defs: THEORY
BEGIN
sign_rep: type = {n:nat| n = 0 or n = 1}
pos:sign_rep = 0
neg:sign_rep = 1
NaN_type: type = {signal,quiet}
NaN_data: NONEMPTY_TYPE
invalid_data: NaN_data
fp_ops : type = {add,sub,mult,div}
rounding_mode : type = {to_nearest,to_zero,to_pos,to_neg}
exception: DATATYPE
BEGIN
invalid_operation : invalid?
division_by_zero : div_by_zero?
overflow : overflow?
underflow(exact?:bool) : underflow?
inexact : inexact?
no_exceptions : no_exceptions?
END exception
trap_enabled?(e:exception) : bool
END enumerated_type_defs
$$$enumerated_type_defs.prf
(|enumerated_type_defs| (|pos_TCC1| "" (ASSERT) NIL)
(|neg_TCC1| "" (ASSERT) NIL))
$$$IEEE_854_remainder.pvs
IEEE_854_remainder
[b,p:above(1),
alpha,E_max:integer,
E_min:{i:integer|E_max>i}]: THEORY
BEGIN
IMPORTING IEEE_854_values[b,p,E_max,E_min],
real_to_fp[b,p,alpha,E_max,E_min],
round
fin, fin1, fin2: var (finite?)
REM(fin1, (fin2:{fin|not zero?(fin)})): fp_num =
let x = value(fin1),
y = value(fin2) in
if (x - y * round_to_even(x/y)) = 0
then finite(sign(fin1),E_min,d_zero)
else real_to_fp(x - y * round_to_even(x/y))
endif
END IEEE_854_remainder
$$$IEEE_854_remainder.prf
(|IEEE_854_remainder| (IMPORTING1_TCC1 "" (INST 1 "E_max - 1") NIL)
(REM_TCC1 "" (SKOLEM-TYPEPRED)
(("" (SKOSIMP*)
(("" (REPLACE -6)
(("" (EXPAND "zero?") (("" (PROPAX) NIL)))))))))
(REM_TCC2 "" (SKOSIMP*) (("" (ASSERT) NIL))))
$$$real_to_fp.pvs
real_to_fp
[b,p:above(1),
alpha,E_max:integer,
E_min:{i:integer|E_max>i}]: THEORY
BEGIN
IMPORTING IEEE_854_values[b,p,E_max,E_min],
over_under[b,p,alpha,E_max,E_min],
fp_round_aux[b,p],
round
r: var real
mode: var rounding_mode
op: var fp_ops
fin, fin1, fin2: var (finite?)
px: var posreal
E: var integer
JUDGEMENT truncate has_type [integer,nonneg_real -> digits]
truncate_zero: lemma truncate(E,0)=d_zero
digits_of_finite: lemma truncate(Exp(fin),abs(value(fin))) = d(fin)
real_to_fp(r): fp_num =
IF abs(r) >= b^(E_max+1) THEN
infinite(sign_of(r))
ELSIF abs(r) < b^E_min THEN
finite(sign_of(r), E_min, truncate(E_min, abs(r)))
ELSE
finite(sign_of(r), Exp_of(abs(r)), truncate(Exp_of(abs(r)), abs(r)))
ENDIF
real_to_fp_x(r:real,e:exception): [fp_num,exception] = (real_to_fp(r),e)
real_to_fp_zero: lemma real_to_fp(0) = pos_zero
sign_of_value: lemma not zero?(fin) =>(sign_of(value(fin))= sign(fin))
Exp_of_value_normal: LEMMA
normal?(fin)
=> Exp_of(abs(value(fin))) = Exp(normalize(fin))
real_to_fp_normal: LEMMA
normal?(fin)
=> real_to_fp(value(fin)) = normalize(fin)
real_to_fp_subnormal: LEMMA
subnormal?(fin)
=> real_to_fp(value(fin)) = normalize(fin)
real_to_fp_inverts_value: LEMMA
not zero?(fin) => real_to_fp(value(fin)) = normalize(fin)
round_exceptions_x(x:(over_under?),mode:rounding_mode): [real,exception] =
IF abs(x)>max_pos THEN
overflow(x,mode)
ELSE underflow(x,mode)
ENDIF
round_exceptions(r:(over_under?),mode): real
= proj_1(round_exceptions_x(r,mode))
fp_round(r, mode): real =
IF r = 0 THEN 0
ELSIF over_under?(r) then
round_exceptions(r,mode)
ELSE round_scaled(r,mode)
ENDIF
is_exact?(r:nzreal,mode):exception =
IF round_scaled(r,mode) = r then no_exceptions ELSE inexact ENDIF
fp_round_x(r, mode): [real,exception] =
IF r = 0 THEN (0,no_exceptions)
ELSIF over_under?(r) then
round_exceptions_x(r,mode)
ELSE (round_scaled(r,mode),is_exact?(r,mode))
ENDIF
round_value: lemma not over_under?(value(fin)) =>
fp_round(value(fin),mode) = value(fin)
round_value2: lemma not trap_enabled?(underflow(FALSE)) =>
fp_round(value(fin),mode) = value(fin)
round_0: lemma fp_round(0,mode)=0
round_value3: lemma not trap_enabled?(underflow(FALSE)) =>
not zero?(fin) =>
real_to_fp(fp_round(value(fin),mode)) = normalize(fin)
round_error: lemma r/=0 & not over_under?(r)
=> abs(r-fp_round(r,mode)) abs(r - fp_round(r, to_nearest))
<= b ^ (Exp_of(abs(r)) - (p - 1)) / 2
round_pos: lemma not over_under?(r) => fp_round(r,to_pos)>=r
round_neg: lemma not over_under?(r) => fp_round(r,to_neg)<=r
round_zero: lemma not over_under?(r) => abs(fp_round(r,to_zero))<=abs(r)
END real_to_fp
$$$real_to_fp.prf
(|real_to_fp|
(|truncate_zero| "" (SKOSIMP*)
(("" (APPLY-EXTENSIONALITY)
(("" (EXPAND "truncate")
(("" (EXPAND "d_zero")
(("" (ASSERT)
(("" (LEMMA "div_eq_zero")
(("" (ASSERT)
(("" (REWRITE "floor_int")
(("" (REWRITE "mod_zero") NIL)))))))))))))))))
(|digits_of_finite| "" (SKOSIMP*)
(("" (REWRITE "abs_value_fin")
(("" (CASE "b ^ (Exp(fin!1)) * Sum(p, value_digit(d(fin!1))) >=0")
(("1" (APPLY-EXTENSIONALITY)
(("1" (HIDE 2)
(("1" (REWRITE "truncate")
(("1" (ASSERT)
(("1"
(CASE-REPLACE "(b ^ (x!1 - Exp(fin!1))
*
(b ^ (Exp(fin!1))
* Sum(p, value_digit(d(fin!1))))) =
Sum(p, value_digit(d(fin!1)))*b^x!1")
(("1" (HIDE -1 -2)
(("1" (LEMMA "floor_Sum")
(("1" (INST?)
(("1" (REPLACE -1)
(("1" (HIDE -1)
(("1" (LEMMA "mod_Sum")
(("1" (INST?) NIL)))))))))))))
("2" (HIDE -1 2)
(("2" (ASSERT)
(("2" (LEMMA "expt_plus")
(("2" (INST?)
(("2" (INST - "Exp(fin!1)")
(("2" (ASSERT) NIL)))))))))))))))))))))
("2" (LEMMA "expt_pos")
(("2" (INST?)
(("2" (LEMMA "Sum_nonneg")
(("2" (INST?)
(("2" (REWRITE "pos_times_ge")
(("2" (ASSERT) NIL)))))))))))))))))
(|real_to_fp_TCC1| "" (TCC :DEFS !) NIL)
(|real_to_fp_TCC2| "" (TCC :DEFS !) NIL)
(|real_to_fp_TCC3| "" (TCC :DEFS !) NIL)
(|real_to_fp_TCC4| "" (SKOSIMP*)
(("" (HIDE 1)
(("" (LEMMA "expt_pos")
(("" (INST?) (("1" (ASSERT) NIL) ("2" (ASSERT) NIL)))))))))
(|real_to_fp_TCC5| "" (SKOSIMP)
(("" (CASE "abs(r!1)>0")
(("1" (TYPEPRED "Exp_of(abs(r!1))")
(("1" (GROUND)
(("1" (CASE "b^E_min<= abs(r!1)")
(("1" (LEMMA "both_sides_expt_gt1_lt")
(("1" (INST - "b" "E_min" "(1 + Exp_of(abs(r!1)))")
(("1" (ASSERT) NIL)))))
("2" (ASSERT) NIL)))
("2" (CASE "abs(r!1)0")
(("1" (ASSERT)
(("1"
(TYPEPRED "Exp_of(b ^ (Exp(normalize(fin!1)))
* Sum(p, value_digit(d(normalize(fin!1)))))")
(("1" (LEMMA "div_mult_pos_lt2")
(("1"
(INST - "b ^ (Exp(normalize(fin!1)))"
"Sum(p, value_digit(d(normalize(fin!1))))"
"b
^
(1
+
Exp_of(b ^ (Exp(normalize(fin!1)))
* Sum(p, value_digit(d(normalize(fin!1))))))")
(("1" (REPLACE -1 :DIR RL)
(("1" (HIDE -1)
(("1"
(LEMMA "div_mult_pos_le1")
(("1"
(INST
-
"b ^ (Exp(normalize(fin!1)))"
"Sum(p, value_digit(d(normalize(fin!1))))"
"b
^
( Exp_of(b ^ (Exp(normalize(fin!1)))
* Sum(p, value_digit(d(normalize(fin!1))))))")
(("1"
(REPLACE -1 :DIR RL)
(("1"
(HIDE -1)
(("1"
(REWRITE "expt_div")
(("1"
(REWRITE "expt_div")
(("1"
(CASE
"(Exp_of(b ^ (Exp(normalize(fin!1)))
* Sum(p, value_digit(d(normalize(fin!1))))))
> (Exp(normalize(fin!1)))")
(("1"
(LEMMA "expt_gt1_pos")
(("1"
(INST
-
"b"
"(Exp_of(b ^ (Exp(normalize(fin!1)))
* Sum(p, value_digit(d(normalize(fin!1))))))
- (Exp(normalize(fin!1)))")
(("1" (ASSERT) NIL)
("2"
(ASSERT)
NIL)))))
("2"
(LEMMA
"expt_gt1_nonpos")
(("2"
(INST
-
"b"
"-((1
+
Exp_of(b ^ (Exp(normalize(fin!1)))
* Sum(p, value_digit(d(normalize(fin!1))))))
- (Exp(normalize(fin!1))))")
(("1" (ASSERT) NIL)
("2"
(ASSERT)
NIL)))))))))))))))))))))))))))))))
("2" (REWRITE "pos_times_gt")
(("2" (ASSERT) NIL)))))))))))))))))))))))))))))
(|real_to_fp_normal| "" (SKOSIMP*)
(("" (REWRITE "real_to_fp")
(("" (LIFT-IF)
(("" (LEMMA "value_normal")
(("" (INST?)
(("" (ASSERT)
(("" (FLATTEN)
(("" (ASSERT)
(("" (CASE "max_pos < b^(1+E_max)")
(("1" (ASSERT)
(("1" (HIDE -1 -2 -3)
(("1" (REWRITE "Exp_of_value_normal")
(("1" (LEMMA "finite_disjoint1")
(("1" (INST?)
(("1" (ASSERT)
(("1" (REWRITE "normal_value")
(("1" (REWRITE "sign_of_value")
(("1" (ASSERT)
(("1" (REWRITE "digits_of_finite")
(("1"
(REWRITE "fp_num_finite_eta")
NIL)))))
("2" (EXPAND "zero?")
(("2" (REWRITE "normal_value" +)
NIL)))))))))))))))))))
("2" (HIDE 2)
(("2" (HIDE -1 -2 -3)
(("2" (LEMMA "max_fp_correct")
(("2" (LEMMA "expt_pos")
(("2" (INST - "(E_max-(p-1))" "b")
(("2" (ASSERT) NIL)))))))))))))))))))))))))))))
(|real_to_fp_subnormal| "" (SKOSIMP*)
(("" (REWRITE "real_to_fp")
(("" (LEMMA "value_subnormal")
(("" (INST?)
(("" (ASSERT)
(("" (FLATTEN)
(("" (ASSERT)
(("" (CASE "b^E_min < b^(1+E_max)")
(("1" (ASSERT)
(("1" (REWRITE "normal_value")
(("1" (REWRITE "sign_of_value")
(("1" (HIDE -1)
(("1" (EXPAND "subnormal?")
(("1" (ASSERT)
(("1" (GROUND)
(("1" (LEMMA "digits_of_finite")
(("1" (INST?)
(("1" (LEMMA "fp_num_finite_eta")
(("1" (INST?)
(("1"
(REPLACE -5)
(("1"
(REPLACE -2)
(("1"
(PROPAX)
NIL)))))))))))))))))))))
("2" (EXPAND "subnormal?")
(("2" (GROUND)
(("2" (EXPAND "zero?")
(("2" (ASSERT)
(("2" (REWRITE "normal_value" +)
NIL)))))))))))))))
("2" (HIDE -1 -2 -3 2)
(("2" (REWRITE "both_sides_expt_gt1_lt")
NIL)))))))))))))))))))
(|real_to_fp_inverts_value| "" (SKOSIMP*)
(("" (LEMMA "finite_cover")
(("" (INST?)
(("" (GROUND)
(("1" (REWRITE "real_to_fp_normal") NIL)
("2" (REWRITE "real_to_fp_subnormal") NIL)))))))))
(|round_exceptions_x_TCC1| "" (SKOLEM-TYPEPRED)
(("" (EXPAND "over_under?") (("" (GROUND) NIL)))))
(|round_exceptions_x_TCC2| "" (SKOLEM-TYPEPRED)
(("" (EXPAND "over_under?") (("" (GROUND) NIL)))))
(|fp_round_TCC1| "" (TCC :DEFS !) NIL)
(|round_value| "" (SKOSIMP*)
(("" (EXPAND "fp_round")
(("" (EXPAND "round_scaled")
(("" (ASSERT)
(("" (LIFT-IF)
(("" (ASSERT)
(("" (GROUND)
(("" (EXPAND "scale")
(("" (REWRITE "Exp_of_value_normal")
(("1" (REWRITE "round_int")
(("1" (REWRITE "expt_inverse") (("1" (ASSERT) NIL)))
("2" (HIDE 2 3 4)
(("2"
(CASE "integer?(value(fin!1)*b^(-(1 + Exp(normalize(fin!1)) - p)))")
(("1" (EXPAND "integer?")
(("1" (ASSERT) (("1" (GROUND) NIL)))))
("2" (HIDE 2)
(("2" (REWRITE "normal_value")
(("2" (EXPAND "value")
(("2"
(CASE-REPLACE
"(Sum(p, value_digit(d(normalize(fin!1))))
* (-1) ^ sign(normalize(fin!1))
* b ^ Exp(normalize(fin!1))
* b ^ (-(1 + Exp(normalize(fin!1)) - p))) =
(-1) ^ sign(normalize(fin!1))
* Sum(p, value_digit(d(normalize(fin!1))))
* b ^ (p-1)")
(("1" (HIDE -1)
(("1"
(CASE-REPLACE
"((-1) ^ sign(normalize(fin!1))
* Sum(p, value_digit(d(normalize(fin!1))))
* b ^ (p - 1)) = ((-1) ^ sign(normalize(fin!1))
* Sum(p, scale_value_p(d(normalize(fin!1)))))")
(("1" (HIDE -1)
(("1"
(CASE
"FORALL (i,j:int): integer?(i*j)")
(("1"
(INST?)
(("1"
(HIDE 2)
(("1"
(CASE
"forall (n:nat),(d:digits): integer?(Sum(n,scale_value_p(d)))")
(("1"
(EXPAND "integer?")
(("1" (INST?) NIL)))
("2"
(HIDE 2)
(("2"
(INDUCT "n")
(("1"
(EXPAND "Sum")
(("1"
(EXPAND "integer?")
(("1" (PROPAX) NIL)))))
("2"
(SKOSIMP*)
(("2"
(REWRITE "Sum")
(("2"
(INST?)
(("2"
(CASE
"FORALL (i,j:int): integer?(i+j)")
(("1"
(INST?)
(("1"
(EXPAND
"integer?")
(("1"
(PROPAX)
NIL)))))
("2"
(HIDE -1 2)
(("2"
(SKOSIMP*)
(("2"
(EXPAND
"integer?")
(("2"
(PROPAX)
NIL)))))))))))))))))))))))))
("2"
(HIDE 2)
(("2"
(SKOSIMP*)
(("2"
(EXPAND "integer?")
(("2" (PROPAX) NIL)))))))))))
("2" (HIDE 2)
(("2"
(ASSERT)
(("2"
(LEMMA "scaled_Sum")
(("2"
(INST?)
(("2" (ASSERT) NIL)))))))))))))
("2" (HIDE 2)
(("2" (ASSERT)
(("2" (LEMMA "expt_plus")
(("2"
(INST
-
"Exp(normalize(fin!1))"
"(-(1+Exp(normalize(fin!1)) - p))"
"b")
(("2"
(ASSERT)
NIL)))))))))))))))))))))))
("2" (HIDE 3)
(("2" (EXPAND "over_under?")
(("2" (LEMMA "value_subnormal")
(("2" (INST?)
(("2" (GROUND)
(("2" (LEMMA "finite_cover")
(("2" (INST?)
(("2" (EXPAND "zero?")
(("2" (PROPAX)
NIL)))))))))))))))))))))))))))))))))))
(|round_value2| "" (SKOSIMP*)
(("" (REWRITE "round_value")
(("" (EXPAND "fp_round")
(("" (LIFT-IF)
(("" (ASSERT)
(("" (PROP)
(("" (EXPAND "round_exceptions")
(("" (EXPAND "round_exceptions_x")
(("" (LEMMA "value_nonzero")
(("" (INST?)
(("" (ASSERT)
(("" (EXPAND "zero?")
(("" (LIFT-IF)
(("" (PROP)
(("1" (ASSERT) NIL)
("2" (EXPAND "over_under?")
(("2" (ASSERT)
(("2" (EXPAND "underflow")
(("2" (LIFT-IF)
(("2" (ASSERT)
(("2"
(REWRITE "round_under_value")
(("2"
(LEMMA "finite_cover")
(("2"
(INST?)
(("2"
(EXPAND "zero?")
(("2"
(LEMMA "value_normal")
(("2"
(INST?)
(("2"
(ASSERT)
NIL)))))))))))))))))))))))))))))))))))))))))))))))))))
(|round_0| "" (SKOSIMP*) (("" (EXPAND "fp_round") (("" (PROPAX) NIL)))))
(|round_value3| "" (SKOSIMP*)
(("" (REWRITE "round_value2")
(("" (REWRITE "real_to_fp_inverts_value") NIL)))))
(|round_error_TCC1| "" (TCC :DEFS !) NIL)
(|round_error_TCC2| "" (TCC :DEFS !) NIL)
(|round_error| "" (SKOSIMP*)
(("" (EXPAND "fp_round")
(("" (EXPAND "round_scaled")
(("" (LIFT-IF)
(("" (GROUND)
((""
(CASE-REPLACE "r!1
- b ^ scale(abs(r!1))
* round(r!1 * b ^ (-scale(abs(r!1))), mode!1)=
b^scale(abs(r!1))*(r!1*b ^ (-scale(abs(r!1))) -round(r!1 * b ^ (-scale(abs(r!1))), mode!1))")
(("1" (HIDE -1)
(("1" (REWRITE "abs_mult")
(("1" (LEMMA "div_mult_pos_lt2")
(("1"
(INST - "abs(b ^ scale(abs(r!1)))"
"abs((r!1 * b ^ (-scale(abs(r!1)))
- round(r!1 * b ^ (-scale(abs(r!1))), mode!1)))"
"b ^ (1 + Exp_of(abs(r!1)) - p)")
(("1" (REPLACE -1 :DIR RL)
(("1" (HIDE -1)
(("1"
(CASE-REPLACE
"b ^ (1 + Exp_of(abs(r!1)) - p) / abs(b ^ scale(abs(r!1)))=1")
(("1" (REWRITE "round1") NIL)
("2" (HIDE 3)
(("2" (HIDE 2)
(("2" (LEMMA "expt_pos")
(("2" (REWRITE "abs")
(("2" (LIFT-IF)
(("2" (GROUND)
(("1"
(REWRITE "abs")
(("1"
(LIFT-IF)
(("1"
(INST?)
(("1"
(ASSERT)
(("1"
(EXPAND "scale")
(("1" (ASSERT) NIL)))))))))))
("2"
(REWRITE "abs")
(("2"
(LIFT-IF)
(("2"
(INST?)
(("2"
(ASSERT)
(("2"
(EXPAND "scale")
(("2"
(ASSERT)
NIL)))))))))))))))))))))))
("3" (HIDE 3)
(("3" (EXPAND "abs" + 1)
(("3" (LEMMA "expt_pos")
(("3" (INST?)
(("3" (ASSERT) NIL)))))))))))))))
("2" (HIDE 3)
(("2" (LEMMA "expt_pos")
(("2" (INST?)
(("2" (EXPAND "abs" + 1)
(("2" (ASSERT) NIL)))))))))))))))))
("2" (HIDE 3)
(("2" (ASSERT)
(("2" (REWRITE "expt_inverse")
(("2" (ASSERT) NIL)))))))))))))))))))
(|round_near| "" (SKOSIMP*)
(("" (EXPAND "fp_round")
(("" (EXPAND "round_scaled")
(("" (ASSERT)
(("" (CASE "abs(r!1)>0")
(("1"
(CASE-REPLACE "(r!1
- b ^ scale(abs(r!1))
* round(r!1 * b ^ (-scale(abs(r!1))), to_nearest)) =
b^scale(abs(r!1))*(r!1*b^(-scale(abs(r!1))) - round(r!1 * b ^ (-scale(abs(r!1))), to_nearest))")
(("1" (HIDE -1)
(("1" (REWRITE "abs_mult")
(("1" (LEMMA "div_mult_pos_le2")
(("1"
(INST - "abs(b ^ scale(abs(r!1)))"
"abs((r!1 * b ^ (-scale(abs(r!1)))
- round(r!1 * b ^ (-scale(abs(r!1))), to_nearest)))"
"b ^ (1 + Exp_of(abs(r!1)) - p) / 2")
(("1" (REPLACE -1 :DIR RL)
(("1" (HIDE -1)
(("1"
(CASE-REPLACE
"b ^ (1 + Exp_of(abs(r!1)) - p) / 2 / abs(b ^ scale(abs(r!1)))=1/2")
(("1" (EXPAND "round")
(("1" (REWRITE "round_to_even1") NIL)))
("2" (HIDE 3)
(("2" (REWRITE "div_div2")
(("1" (EXPAND "scale")
(("1" (EXPAND "abs" + 2)
(("1" (LIFT-IF)
(("1" (LEMMA "expt_pos")
(("1"
(INST?)
(("1" (ASSERT) NIL)))))))))))
("2" (HIDE 2)
(("2" (LEMMA "expt_pos")
(("2" (INST?)
(("2" (EXPAND "abs" + 1)
(("2" (ASSERT) NIL)))))))))))))
("3" (HIDE 3)
(("3" (LEMMA "expt_pos")
(("3" (INST?)
(("3" (EXPAND "abs" + 1)
(("3" (ASSERT) NIL)))))))))))))))
("2" (HIDE 3)
(("2" (LEMMA "expt_pos")
(("2" (INST?)
(("2" (EXPAND "abs" + 1)
(("2" (ASSERT) NIL)))))))))))))))))
("2" (ASSERT)
(("2" (HIDE 3)
(("2" (REWRITE "expt_inverse") (("2" (ASSERT) NIL)))))))))
("2" (HIDE 3)
(("2" (EXPAND "abs")
(("2" (LIFT-IF) (("2" (ASSERT) NIL)))))))))))))))))
(|round_pos| "" (SKOSIMP*)
(("" (EXPAND "fp_round")
(("" (EXPAND "round_scaled")
(("" (LIFT-IF)
(("" (ASSERT)
(("" (GROUND)
(("" (EXPAND "round")
(("" (ASSERT)
(("" (LEMMA "div_mult_pos_ge2")
((""
(INST - "b ^ scale(abs(r!1))"
"ceiling(r!1 * b ^ (-scale(abs(r!1))))" "r!1")
(("1" (REPLACE -1 :DIR RL)
(("1" (REWRITE "expt_inverse") (("1" (ASSERT) NIL)))))
("2" (LEMMA "expt_pos")
(("2" (INST?)
(("2" (ASSERT) NIL)))))))))))))))))))))))))
(|round_neg| "" (SKOSIMP*)
(("" (EXPAND "fp_round")
(("" (EXPAND "round_scaled")
(("" (LIFT-IF)
(("" (GROUND)
(("" (EXPAND "round")
(("" (LEMMA "div_mult_pos_le2")
((""
(INST - "b ^ scale(abs(r!1))"
"floor(r!1 * b ^ (-scale(abs(r!1))))" "r!1")
(("1" (REPLACE -1 :DIR RL)
(("1" (REWRITE "expt_inverse")
(("1" (HIDE -1)
(("1"
(TYPEPRED "floor(r!1 * (1 / (b ^ scale(abs(r!1)))))")
(("1" (ASSERT) NIL)
("2" (SKOSIMP)
(("2" (LEMMA "expt_pos")
(("2" (INST?) (("2" (ASSERT) NIL)))))))
("3" (SKOSIMP*)
(("3" (LEMMA "expt_nonzero")
(("3" (INST?) (("3" (ASSERT) NIL)))))))
("4" (REWRITE "expt_nonzero") NIL)))))))))
("2" (LEMMA "expt_pos")
(("2" (INST?) (("2" (ASSERT) NIL)))))))))))))))))))))
(|round_zero| "" (SKOSIMP*)
(("" (EXPAND "fp_round")
(("" (ASSERT)
(("" (LIFT-IF)
(("" (PROP)
(("1" (ASSERT) NIL)
("2" (CASE "abs(r!1)>0")
(("1" (HIDE 3)
(("1" (EXPAND "round_scaled")
(("1" (REWRITE "abs_mult")
(("1" (NAME-REPLACE "sr!1" "scale(abs(r!1))")
(("1" (REWRITE "expt_inverse")
(("1" (LEMMA "expt_pos")
(("1" (INST?)
(("1" (NAME-REPLACE "s!1" "b^sr!1")
(("1" (CASE "abs(s!1)>0")
(("1" (LEMMA "div_mult_pos_le2")
(("1"
(INST - "abs(s!1)"
"abs(round(r!1/s!1,to_zero))" "abs(r!1)")
(("1" (REPLACE -1 :DIR RL)
(("1" (HIDE -1)
(("1"
(CASE-REPLACE
"abs(r!1) / abs(s!1) = abs(r!1/s!1)")
(("1"
(HIDE -1)
(("1"
(NAME-REPLACE "r!2" "r!1/s!1")
(("1"
(HIDE -1 -2 -3 1)
(("1" (GRIND) NIL)))
("2" (ASSERT) NIL)))))
("2"
(HIDE -3 2 3)
(("2"
(GRIND)
(("1" (REWRITE "neg_div_lt") NIL)
("2"
(REWRITE "neg_div_lt")
NIL)))))
("3" (ASSERT) NIL)
("4" (ASSERT) NIL)))))))
("2" (ASSERT) NIL)))))
("2" (HIDE -2 2 3)
(("2" (EXPAND "abs")
(("2" (LIFT-IF)
(("2" (ASSERT)
NIL)))))))))))))))))))))))))
("2" (HIDE 3 4) (("2" (GRIND) NIL))))))))))))))))
$$$over_under.pvs
over_under
[b,p:above(1),
alpha,E_max:integer,
E_min:{i:integer|E_max>i}]: THEORY
BEGIN
IMPORTING IEEE_854_values[b,p,E_max,E_min],
fp_round_aux[b,p],
enumerated_type_defs,
round
over_under?(r:real): bool = (r/=0 & (abs(r)>max_pos or abs(r) max_pos), (mode: rounding_mode)):
[real, exception] =
CASES mode OF
to_nearest:
IF abs(r)
>= b ^ (E_max + 1)
- (1 / 2) * b ^ (E_max + 1 - p)
THEN (trap_over(r, (sgn(r) * infinity), mode),overflow)
ELSE (sgn(r) * max_pos, inexact)
ENDIF,
to_zero:
IF abs(r) >= b ^ (E_max + 1)
THEN (trap_over(r, (sgn(r) * max_pos), mode),overflow)
ELSE (sgn(r) * max_pos, inexact)
ENDIF,
to_pos:
IF r > max_pos THEN (trap_over(r, infinity, mode),overflow)
ELSIF r <= -b ^ (E_max + 1)
THEN (trap_over(r, max_neg, mode),overflow)
ELSE (max_neg, inexact)
ENDIF,
to_neg:
IF r < max_neg THEN (trap_over(r, -infinity, mode),overflow)
ELSIF r >= b ^ (E_max + 1)
THEN (trap_over(r, max_pos, mode),overflow)
ELSE (max_pos, inexact)
ENDIF
ENDCASES
tiny_flag: bool % = true for tininess detected after rounding
inaccurate_flag: bool % = true for inaccurate detected using first option
exact_underflow((r:nzreal|abs(r)
round_under(value(fin),mode) = value(fin)
r:var nzreal
round_under_error: LEMMA
abs(r) < b ^ E_min
=> abs(r - round_under(r, mode)) < b ^ (E_min - (p - 1))
round_under_near: LEMMA
abs(r) < b ^ E_min
=> abs(r - round_under(r, to_nearest)) <= b ^ (E_min - (p - 1)) / 2
round_under_pos: lemma abs(r) round_under(r,to_pos)>=r
round_under_neg: lemma abs(r) round_under(r,to_neg)<=r
round_under_zero: lemma abs(r) abs(round_under(r,to_zero))<=abs(r)
inaccurate?((r: nzreal | abs(r) < b ^ E_min), (mode: rounding_mode)): bool =
IF inaccurate_flag THEN (round_scaled(r,mode)/=round_under(r,mode))
ELSE (r/=round_under(r,mode))
ENDIF
underflow((r: nzreal | abs(r) < b ^ E_min), (mode: rounding_mode)):
[real, exception] =
IF tiny?(r, mode)
THEN IF trap_enabled?(underflow(FALSE))
THEN (round_scaled(r * b ^ alpha, mode),
underflow(exact_underflow(r, mode)))
ELSIF inaccurate?(r, mode) THEN (round_under(r, mode), underflow(TRUE))
ELSE (round_under(r, mode),
IF r = round_under(r, mode) THEN no_exceptions
ELSE inexact
ENDIF)
ENDIF
ELSE (round_under(r, mode), inexact)
ENDIF
END over_under
$$$over_under.prf
(|over_under| (|over_under?_TCC1| "" (TCC :DEFS !) NIL)
(|infinity_TCC1| "" (TCC :DEFS !) NIL)
(|trap_over_TCC1| "" (TCC :DEFS !) NIL)
(|trap_over_TCC2| "" (SKOSIMP*)
(("" (REWRITE "zero_times3")
(("" (LEMMA "expt_nonzero") (("" (INST?) (("" (ASSERT) NIL)))))))))
(|overflow_TCC1| "" (TCC :DEFS !) NIL) (|overflow_TCC2| "" (TCC :DEFS !) NIL)
(|overflow_TCC3| "" (TCC) NIL) (|overflow_TCC4| "" (TCC :DEFS !) NIL)
(|overflow_TCC5| "" (TCC :DEFS !) NIL)
(|exact_underflow_TCC1| "" (TCC :DEFS !) NIL)
(|exact_underflow_TCC2| "" (SKOLEM-TYPEPRED)
(("1" (HIDE -2)
(("1" (USE "expt_nonzero")
(("1" (ASSERT) (("1" (PROP) (("1" (REWRITE "zero_times3") NIL)))))
("2" (ASSERT) NIL)))))
("2" (SKOSIMP*) (("2" (ASSERT) NIL)))))
(|tiny?_TCC1| "" (SUBTYPE-TCC) NIL) (|round_under_TCC1| "" (TCC :DEFS !) NIL)
(|round_under_TCC2| "" (TCC :DEFS !) NIL)
(|round_under_correct_TCC1| "" (ASSERT)
(("" (EXPAND "min_pos")
(("" (LEMMA "min_fp_correct")
(("" (REPLACE -1)
(("" (HIDE -1)
(("" (LEMMA "expt_pos")
(("" (INST?)
(("" (ASSERT)
(("" (EXPAND "abs")
(("" (LEMMA "expt_plus")
(("" (INST - "E_min" "1-p" "b")
(("" (REPLACE -1)
(("" (HIDE -1)
(("" (LEMMA "both_sides_times_pos_lt2")
(("" (INST - "b^E_min" "b^(1-p)" "1")
(("1" (LEMMA "expt_gt1_neg")
(("1" (INST - "b" "p-1")
(("1" (GROUND) NIL)))))
("2" (LEMMA "expt_pos")
(("2" (INST?)
(("2" (ASSERT)
NIL)))))))))))))))))))))))))))))))))))
(|round_under_correct| "" (SKOSIMP*)
(("" (EXPAND "round_under")
(("" (REWRITE "round_int")
(("1" (LEMMA "expt_plus")
(("1" (INST - "(1 + E_min - p)" "(-(1 + E_min - p))" "b")
(("1" (REWRITE "expt_x0")
(("1" (REWRITE "associative_mult") (("1" (ASSERT) NIL)))))))))
("2" (HIDE 2)
(("2" (EXPAND "min_pos")
(("2" (LEMMA "min_fp_correct")
(("2" (REPLACE -1)
(("2" (HIDE -1)
(("2" (REWRITE "expt_plus" :DIR RL)
(("2" (REWRITE "expt_x0")
(("2" (ASSERT) NIL)))))))))))))))))))))
(|round_under_value_TCC1| "" (SKOSIMP*)
(("" (PROP)
(("1" (EXPAND "subnormal?") (("1" (EXPAND "zero?") (("1" (GROUND) NIL)))))
("2" (LEMMA "value_subnormal") (("2" (INST?) (("2" (ASSERT) NIL)))))))))
(|round_under_value| "" (SKOSIMP*)
(("" (EXPAND "round_under")
(("" (REWRITE "round_int")
(("1" (LEMMA "expt_plus")
(("1" (INST - "(1 + E_min - p)" "(-(1 + E_min - p))" "b")
(("1" (REWRITE "expt_x0")
(("1" (GROUND)
(("1" (REWRITE "associative_mult")
(("1" (ASSERT)
(("1" (REWRITE "associative_mult" :DIR RL)
(("1" (ASSERT) NIL)))))))))))))))
("2" (HIDE 2)
(("2"
(CASE "integer?(b ^ (-(1 + E_min - p))
* value(fin!1))")
(("1" (EXPAND "integer?") (("1" (PROPAX) NIL)))
("2" (HIDE 2)
(("2" (EXPAND "subnormal?")
(("2" (REWRITE "normal_value")
(("2" (EXPAND "value")
(("2" (PROP)
(("2" (REPLACE -1)
(("2" (ASSERT)
(("2"
(CASE-REPLACE "b ^ (-(1 + E_min - p))
*
(Sum(p, value_digit(d(normalize(fin!1))))
* (-1) ^ sign(normalize(fin!1))
* b ^ E_min) =
(-1)^sign(normalize(fin!1)) *(Sum(p,scale_value_p(d(normalize(fin!1)))))")
(("1" (HIDE -1)
(("1" (ASSERT)
(("1"
(CASE-REPLACE
"scale_value_p(d(normalize(fin!1))) = scale_value(d(normalize(fin!1)),p-1)")
(("1" (HIDE -1)
(("1" (LEMMA "scaled_Sum_int")
(("1" (INST?)
(("1"
(CASE
"FORALL (i,j:int): integer?(i*j)")
(("1"
(INST?)
(("1"
(EXPAND "integer?")
(("1" (PROPAX) NIL)))))
("2"
(HIDE -1 -2 -3 2 3)
(("2"
(EXPAND "integer?")
(("2" (PROPAX) NIL)))))))))))))
("2" (HIDE -1 -2 2 3)
(("2" (APPLY-EXTENSIONALITY)
(("1" (EXPAND "scale_value_p")
(("1" (PROPAX) NIL)))
("2" (EXPAND "scale_value")
(("2"
(EXPAND "value_digit")
(("2"
(HIDE 2)
(("2"
(SKOSIMP*)
(("2"
(LIFT-IF)
(("2"
(ASSERT)
(("2"
(REWRITE
"associative_mult"
:DIR
RL)
(("2"
(REWRITE
"expt_plus"
:DIR
RL)
(("2"
(GROUND)
(("1"
(REWRITE
"closed_times")
(("1"
(REWRITE
"closed_times")
(("1"
(CASE
"forall (n:nat): integer_pred(b^n)")
(("1" (INST?) NIL)
("2"
(SKOSIMP*)
(("2"
(ASSERT)
NIL)))))))))
("2"
(REWRITE
"pos_times_ge")
(("2"
(LEMMA "expt_pos")
(("2"
(INST?)
(("2"
(ASSERT)
NIL)))))))))))))))))))))))))))))))))))
("2" (HIDE -1 -2 2 3)
(("2" (ASSERT)
(("2" (LEMMA "scaled_Sum")
(("2" (INST?)
(("2" (REPLACE -1 :DIR RL)
(("2" (HIDE -1)
(("2"
(LEMMA "expt_plus")
(("2"
(INST
-
"E_min"
"(-(1 + E_min - p))"
"b")
(("2"
(REPLACE -1)
(("2"
(ASSERT)
NIL)))))))))))))))))))))))))))))))))))))))))))))
(|round_under_error_TCC1| "" (TCC :DEFS !) NIL)
(|round_under_error_TCC2| "" (SUBTYPE-TCC) NIL)
(|round_under_error| "" (SKOSIMP*)
(("" (EXPAND "round_under")
((""
(CASE-REPLACE "abs(r!1
- b ^ (1 + E_min - p)
* round(b ^ (-(1 + E_min - p)) * r!1, mode!1)) =
abs(b ^ (1 + E_min - p)) * abs( r!1*b ^ (-(1 + E_min - p)) - round(b ^ (-(1 + E_min - p)) * r!1, mode!1))")
(("1" (HIDE -1 -2)
(("1" (REWRITE "abs")
(("1" (LEMMA "expt_pos")
(("1" (INST?)
(("1" (ASSERT)
(("1" (LEMMA "both_sides_times_pos_lt2")
(("1" (INST - "b^(1+E_min-p)" "_" "1")
(("1" (INST?)
(("1" (LEMMA "round1")
(("1" (INST?) (("1" (ASSERT) NIL)))))))))))))))))))))
("2" (HIDE -1 2)
(("2" (REWRITE "abs_mult" :DIR RL)
(("2" (REWRITE "expt_plus" :DIR RL)
(("2" (REWRITE "expt_x0") (("2" (ASSERT) NIL)))))))))
("3" (ASSERT) NIL) ("4" (ASSERT) NIL)))))))
(|round_under_near| "" (SKOSIMP*)
(("" (EXPAND "round_under")
(("" (HIDE -1)
((""
(CASE-REPLACE "abs(r!1
- b ^ (1 + E_min - p)
* round(b ^ (-(1 + E_min - p)) * r!1, to_nearest)) =
abs(b ^ (1 + E_min - p)) * abs( r!1*b ^ (-(1 + E_min - p)) - round(b ^ (-(1 + E_min - p)) * r!1, to_nearest))")
(("1" (HIDE -1)
(("1" (EXPAND "abs" + 1)
(("1" (LEMMA "expt_pos")
(("1" (INST?)
(("1" (ASSERT)
(("1" (LEMMA "both_sides_times_pos_lt2")
(("1" (INST - "b^(1+E_min-p)" "_" "1/2")
(("1" (EXPAND "round")
(("1" (INST?)
(("1" (REWRITE "times_div1")
(("1" (LEMMA "round_to_even1")
(("1" (INST?)
(("1" (ASSERT) NIL)))))))))))))))))
("2" (ASSERT)
(("2" (SPLIT)
(("1" (ASSERT) NIL) ("2" (ASSERT) NIL)))))))))))))
("2" (HIDE 2)
(("2" (REWRITE "abs_mult" :DIR RL)
(("2" (REWRITE "expt_plus" :DIR RL)
(("2" (REWRITE "expt_x0") (("2" (ASSERT) NIL)))))))))
("3" (ASSERT) NIL) ("4" (ASSERT) NIL)))))))))
(|round_under_pos| "" (SKOSIMP*)
(("" (EXPAND "round_under")
(("" (HIDE -1)
(("" (EXPAND "round")
(("" (LEMMA "both_sides_times_pos_ge2")
(("" (LEMMA "expt_pos")
(("" (INST - "(-(1 + E_min - p))" "b")
(("1"
(INST - "b ^ (-(1 + E_min - p))"
"b ^ (1 + E_min - p) * ceiling(b ^ (-(1 + E_min - p)) * r!1)"
"r!1")
(("1" (REPLACE -2 :DIR RL)
(("1" (HIDE -2)
(("1" (REWRITE "associative_mult")
(("1" (REWRITE "associative_mult" :DIR RL)
(("1" (REWRITE "expt_plus" :DIR RL)
(("1" (REWRITE "expt_x0")
(("1" (ASSERT) NIL)))))))))))))
("2" (ASSERT) NIL) ("3" (ASSERT) NIL) ("4" (ASSERT) NIL)))
("2" (ASSERT) NIL)))))))))))))))
(|round_under_neg| "" (SKOSIMP*)
(("" (HIDE -1)
(("" (EXPAND "round_under")
(("" (EXPAND "round")
(("" (LEMMA "both_sides_times_pos_le2")
((""
(INST - "b ^ (-(1 + E_min - p))"
"b ^ (1 + E_min - p) * floor(b ^ (-(1 + E_min - p)) * r!1)"
"r!1")
(("1" (REPLACE -1 :DIR RL)
(("1" (HIDE -1)
(("1" (REWRITE "associative_mult")
(("1" (REWRITE "associative_mult" :DIR RL)
(("1" (REWRITE "expt_plus" :DIR RL)
(("1" (REWRITE "expt_x0")
(("1" (ASSERT) NIL)))))))))))))
("2" (ASSERT) NIL)
("3" (LEMMA "expt_pos")
(("3" (INST?) (("1" (ASSERT) NIL) ("2" (ASSERT) NIL)))))
("4" (ASSERT) NIL)))))))))))))
(|round_under_zero| "" (SKOSIMP*)
(("" (EXPAND "round_under")
(("" (REWRITE "abs_mult")
(("" (EXPAND "round")
(("" (CASE "forall (r1,r2:real): abs(sgn(r1)*r2) = abs(r2)")
(("1" (INST?)
(("1" (REPLACE -1)
(("1" (HIDE -1)
(("1"
(CASE "forall (r:real): abs(floor(abs(r)))=floor(abs(r))")
(("1" (INST?)
(("1" (REPLACE -1)
(("1" (HIDE -1)
(("1" (LEMMA "both_sides_times_pos_le2")
(("1"
(INST - "abs(b ^ (-(1 + E_min - p)))"
"abs(b ^ (1 + E_min - p)) * floor(abs(b ^ (-(1 + E_min - p)) * r!1))"
"abs(r!1)")
(("1" (REPLACE -1 :DIR RL)
(("1" (HIDE -1)
(("1" (HIDE -1)
(("1" (REWRITE "abs_mult" :DIR RL)
(("1" (REWRITE "associative_mult")
(("1"
(REWRITE "associative_mult" :DIR RL)
(("1"
(REWRITE "abs_mult" :DIR RL)
(("1"
(REWRITE "expt_plus" :DIR RL)
(("1"
(REWRITE "expt_x0")
(("1"
(EXPAND "abs" + 2)
(("1"
(ASSERT)
NIL)))))))))))))))))))))
("2" (HIDE -1 2)
(("2" (LEMMA "expt_pos")
(("2" (INST?)
(("2" (EXPAND "abs")
(("2" (ASSERT) NIL)))))))))))))))))))
("2" (HIDE -1 2) (("2" (GRIND) NIL)))))))))))
("2" (HIDE -1 2) (("2" (TCC) NIL)))))))))))))
(|underflow_TCC1| "" (TCC :DEFS !) NIL)
(|underflow_TCC2| "" (SKOSIMP*)
(("" (REWRITE "zero_times3")
(("" (LEMMA "expt_pos") (("" (INST?) (("" (ASSERT) NIL))))))))))
$$$fp_round_aux.pvs
fp_round_aux[b,p:above(1)]: THEORY
BEGIN
importing round,
enumerated_type_defs
r: var real
x: var posreal
sign_of(r:real): sign_rep = IF r < 0 THEN neg ELSE pos ENDIF
Exp_of(x:posreal): {i:int| b^i<= x & x < b^(i+1)}
Exp_of_correct: lemma
1 <= x*b^(-Exp_of(x)) & x*b^(-Exp_of(x)) < b
norm_fp_range: type = {x:posreal | 1 <= x & x < b}
n1: var norm_fp_range
z: var nzreal
E(z):integer = Exp_of(abs(z))
significand(z):norm_fp_range = abs(z)*b^(-Exp_of(abs(z)))
real_components: lemma
z = sgn(z)* b^E(z) * significand(z)
abs_real_components: LEMMA
abs(z) = b^E(z)*significand(z)
i,j: var integer
Exp_of_unique: LEMMA
b^i <= x & x < b^(i+1) & b^j<=x & x i=j
posreal_exponent: lemma
x = b^i *n1 => E(x) = i
real_exponent: lemma
z = sgn(z)*b^i * n1 => E(z) = i
scale(x:posreal):{i:int|b^(i+p-1)<=x & x < b^(i+p)} = Exp_of(x)-(p-1)
scale_correct: lemma b^(p-1)<=x/b^scale(x) & x/b^scale(x)< b^p
round_scaled(r:nzreal,mode:rounding_mode): real =
b^(scale(abs(r)))*round( b^(-scale(abs(r)))*r,mode)
E1: var integer
px: var posreal
nnx: var nonneg_real
truncate(E1,nnx): [below(p)->below(b)] =
(lambda (i:below(p)): mod(floor(b^(i-E1)*nnx),b))
truncate_shift: LEMMA
truncate(i,b^j*px) = truncate(i-j,px)
Exp_of_shift: LEMMA
Exp_of(b^j*px) = j + Exp_of(px)
scale_shift: LEMMA
scale(b^j*px) = j + scale(px)
END fp_round_aux
$$$fp_round_aux.prf
(|fp_round_aux| (|Exp_of_TCC1| "" (TCC :DEFS !) NIL)
(|Exp_of_TCC2| "" (TCC :DEFS !) NIL)
(|Exp_of_TCC3| ""
(INST + "lambda (px:posreal): choose({i:int|b^i<=px & px integer]
%
% Rounds a real number to the nearest integer in accordance
% with the rounding mode (as specified in IEEE-854).
% The function round can be used in two parts of the IEEE-854
% floating point standard.
% 1.) Round floating point to integral value (section 5.5)
% or for converting a floating point to integer (5.4).
% 2.) By giving function `round' an appropriately scaled
% argument, this function can be used in the process
% of converting a real number to a floating point
% representation.
%
% round_to_even:[real -> integer]
%
% Auxilliary function used in definition of round. Selects the
% integer nearest in value to the real argument.
% If the real number is exactly halfway between two integers,
% this function selects the nearest even integer.
% Can also be used:
% -- As an auxilliary function in the definition of
% the remainder function (section 5.1). For y/=0,
% x REM y =def= x - y*n, where n = round_to_even(x/y).
%
%
% Author:
% Paul S. Miner | email: p.s.miner@larc.nasa.gov
% 1 South Wright St. / MS 130 | fax: (804) 864-4234
% NASA Langley Research Center | phone: (804) 864-6201
% Hampton, Virginia 23681 |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Requires library `floor'
BEGIN
importing enumerated_type_defs
% rounding_mode:type = {to_nearest,to_zero,to_pos,to_neg}
mode: var rounding_mode
r: VAR real
round_to_even(r): integer =
IF r - floor(r) < ceiling(r) - r THEN floor(r)
ELSIF ceiling(r) - r < r - floor(r) THEN ceiling(r)
ELSIF floor(r) = ceiling(r) THEN floor(r)
ELSE 2 * floor(ceiling(r) / 2)
ENDIF
round_to_even0: lemma round_to_even(0)=0
round_to_even1: LEMMA abs(r - round_to_even(r)) <= 1 / 2
round_to_even2: LEMMA
abs(r - round_to_even(r)) = 1 / 2 => integer?(round_to_even(r) / 2)
round(r,mode): integer =
CASES mode of
to_nearest: round_to_even(r),
to_zero: sgn(r) * floor(abs(r)),
to_pos: ceiling(r),
to_neg: floor(r)
ENDCASES
round1: LEMMA abs(r-round(r,mode))<1
i:var int
round_int: LEMMA round(i,mode)=i
END round
$$$round.prf
(|round| (|round_to_even0| "" (GRIND) NIL)
(|round_to_even1| "" (SKOSIMP*)
(("" (EXPAND "abs")
(("" (LIFT-IF)
(("" (PROP)
(("1" (EXPAND "round_to_even")
(("1" (LIFT-IF) (("1" (GROUND) NIL)))))
("2" (EXPAND "round_to_even")
(("2" (LIFT-IF) (("2" (GROUND) NIL)))))))))))))
(|round_to_even2| "" (SKOSIMP*)
(("" (EXPAND "abs")
(("" (LIFT-IF)
(("" (PROP)
(("1" (EXPAND "round_to_even")
(("1" (LIFT-IF)
(("1" (GROUND)
(("1" (EXPAND "integer?") (("1" (PROPAX) NIL)))))))))
("2" (EXPAND "round_to_even")
(("2" (LIFT-IF)
(("2" (GROUND)
(("2" (EXPAND "integer?")
(("2" (PROPAX) NIL)))))))))))))))))
(|round1| "" (SKOSIMP*)
(("" (EXPAND "round")
(("" (LIFT-IF)
(("" (PROP)
(("1" (LEMMA "round_to_even1")
(("1" (INST?) (("1" (ASSERT) NIL)))))
("2" (GRIND) NIL) ("3" (GRIND) NIL)
("4" (GRIND) NIL)))))))))
(|round_int| "" (SKOSIMP*)
(("" (EXPAND "round")
(("" (LIFT-IF)
(("" (GROUND)
(("1" (EXPAND "round_to_even")
(("1" (LIFT-IF) (("1" (GROUND) NIL)))))
("2" (EXPAND "abs")
(("2" (LIFT-IF)
(("2" (EXPAND "sgn") (("2" (GROUND) NIL))))))))))))))))
$$$IEEE_854_fp_int.pvs
IEEE_854_fp_int
[b,p:above(1),
alpha,E_max:integer,
E_min:{i:integer|E_max>i}]: THEORY
BEGIN
importing IEEE_854_values[b,p,E_max,E_min],
real_to_fp[b,p,alpha,E_max,E_min],
round
fin, fin1: var (finite?)
mode: var rounding_mode
fp_to_int(fin,mode):integer = round(value(fin),mode)
fp_to_int_fp(fin,mode): fp_num =
real_to_fp(round(value(fin),mode))
% large_value: lemma
% abs(value(fin)) >= b^p => integer?(value(fin))
%
% fp_to_int_fp_finite: lemma
% E_max>p => finite?(real_to_fp(round(value(fin),mode)))
END IEEE_854_fp_int
$$$IEEE_854_fp_int.prf
(|IEEE_854_fp_int| (IMPORTING1_TCC1 "" (INST 1 "E_max - 1") NIL))
$$$arithmetic_ops.pvs
arithmetic_ops
[b,p:above(1),
alpha,E_max:integer,
E_min:{i:integer|E_max>i}]: THEORY
BEGIN
IMPORTING IEEE_854_values[b,p,E_max,E_min],
real_to_fp[b,p,alpha,E_max,E_min],
enumerated_type_defs
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% fp_op provides a template for defining a floating point operation
% for the case when both arguments are finites.
fin,fin1,fin2: var (finite?)
op: var fp_ops
mode: var rounding_mode
apply(op,fin1,(fin2:{fin| div?(op) => not zero?(fin)})): real =
cases op of
add: value(fin1) + value(fin2),
sub: value(fin1) - value(fin2),
mult: value(fin1) * value(fin2),
div: value(fin1) / value(fin2)
endcases
signed_zero(op, fin1, fin2, mode): {fin | zero?(fin)} =
CASES op OF
add:
IF zero?(fin1)
& zero?(fin2) & sign(fin1) = sign(fin2) THEN fin1
ELSIF to_neg?(mode) THEN neg_zero
ELSE pos_zero
ENDIF,
sub:
IF zero?(fin1)
& zero?(fin2) & sign(fin1) /= sign(fin2) THEN fin1
ELSIF to_neg?(mode) THEN neg_zero
ELSE pos_zero
ENDIF,
mult:
IF sign(fin1) = sign(fin2) THEN pos_zero
ELSE neg_zero
ENDIF,
div:
IF sign(fin1) = sign(fin2) THEN pos_zero
ELSE neg_zero
ENDIF
ENDCASES
fp_op(op, fin1, (fin2: {fin | div?(op) => NOT zero?(fin)}), mode): fp_num =
LET r = fp_round(apply(op, fin1, fin2), mode)
IN IF r = 0 THEN signed_zero(op, fin1, fin2, mode)
ELSE real_to_fp(r)
ENDIF
fp_op_x(op,fin1,(fin2:{fin| div?(op) => not zero?(fin)}),mode):
[fp_num, exception]
=
LET rp = fp_round_x(apply(op, fin1, fin2), mode)
IN IF proj_1(rp) = 0 THEN (signed_zero(op, fin1, fin2, mode),proj_2(rp))
ELSE real_to_fp_x(rp)
ENDIF
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
END arithmetic_ops
$$$arithmetic_ops.prf
(|arithmetic_ops| (IMPORTING1_TCC1 "" (INST 1 "E_max - 1") NIL)
(|apply_TCC1| "" (SKOLEM-TYPEPRED) (("" (TCC) NIL)))
(|signed_zero_TCC1| "" (SKOSIMP*) NIL)
(|signed_zero_TCC2| "" (SKOSIMP*) NIL))
$$$comparison1.pvs
comparison1
[b,p:above(1),
E_max:integer,
E_min:{i:integer|E_max>i}]: THEORY
BEGIN
IMPORTING IEEE_854_values[b,p,E_max,E_min]
num,num1,num2: var {fp:fp_num| finite?(fp) or infinite?(fp)}
% extend value function so that infinities can be compared to finite
% numbers
n_value(num): real =
IF infinite?(num) THEN (-1) ^ i_sign(num) * b ^ (E_max + 1)
ELSE value(num)
ENDIF
% From section 5.7 of IEEE-854:
% ``Four mutually exclusive relations are possible: "less than,"
% "equal," "greater than," and "unordered." The last case arises only
% when at least one operand is a NaN.'' ...
% ``The result of a comparison shall be delivered in one of two ways at
% the implementor's option: either as a condition code identifying one
% of the four relations listed above, or as a true/false response to a
% predicate that names the specific comparison desired.''
% fp_compare, below, defines the first option:
comparison_code: type = {gt, lt, eq, un}
fp_compare((fp1, fp2: fp_num)): comparison_code =
IF NaN?(fp1) OR NaN?(fp2) THEN un
ELSIF n_value(fp1) > n_value(fp2) THEN gt
ELSIF n_value(fp1) < n_value(fp2) THEN lt
ELSE eq
ENDIF
fp,fp1,fp2: var fp_num
posinf_ge: LEMMA
gt?(fp_compare(infinite(pos), num))
OR eq?(fp_compare(infinite(pos), num))
NaN_unordered: LEMMA
NaN?(fp1) OR NaN?(fp2) => un?(fp_compare(fp1, fp2))
% option 2, minimal set of predicates is {eq, ne, gt, ge, lt, le} also
% should include un. These predicates are defined below the level
% where invalid will be signalled.
% The follwing predicates are from table 3, page 12 of IEEE-854. They
% do not include the signalling of the invalid exception. That test
% may be applied prior to invoking these predicates.
% shall include
eq?(fp1,fp2) :bool = eq?(fp_compare(fp1,fp2))
ne?(fp1,fp2) :bool = not eq?(fp_compare(fp1,fp2))
gt?(fp1,fp2) :bool = gt?(fp_compare(fp1,fp2))
ge?(fp1,fp2) :bool = gt?(fp_compare(fp1,fp2)) or eq?(fp_compare(fp1,fp2))
lt?(fp1,fp2) :bool = lt?(fp_compare(fp1,fp2))
le?(fp1,fp2) :bool = lt?(fp_compare(fp1,fp2)) or eq?(fp_compare(fp1,fp2))
% should include
un?(fp1,fp2) :bool = un?(fp_compare(fp1,fp2))
% other
lg?(fp1,fp2) :bool = gt?(fp_compare(fp1,fp2)) or lt?(fp_compare(fp1,fp2))
leg?(fp1,fp2):bool = not un?(fp_compare(fp1,fp2))
ug?(fp1,fp2) :bool = gt?(fp_compare(fp1,fp2)) or un?(fp_compare(fp1,fp2))
uge?(fp1,fp2):bool = not lt?(fp_compare(fp1,fp2))
ul?(fp1,fp2) :bool = lt?(fp_compare(fp1,fp2)) or un?(fp_compare(fp1,fp2))
ule?(fp1,fp2):bool = not gt?(fp_compare(fp1,fp2))
ue?(fp1,fp2) :bool = eq?(fp_compare(fp1,fp2)) or un?(fp_compare(fp1,fp2))
eq_def: lemma eq?(num1,num2) <=> n_value(num1) = n_value(num2)
ne_def: lemma ne?(num1,num2) <=> n_value(num1) /= n_value(num2)
gt_def: lemma gt?(num1,num2) <=> n_value(num1) > n_value(num2)
ge_def: lemma ge?(num1,num2) <=> n_value(num1) >= n_value(num2)
lt_def: lemma lt?(num1,num2) <=> n_value(num1) < n_value(num2)
le_def: lemma le?(num1,num2) <=> n_value(num1) <= n_value(num2)
un_def: lemma un?(fp1,fp2) <=> (NaN?(fp1) or NaN?(fp2))
END comparison1
$$$comparison1.prf
(|comparison1| (IMPORTING1_TCC1 "" (INST 1 "E_max - 1") NIL)
(|n_value_TCC1| "" (TCC :DEFS !) NIL)
(|n_value_TCC2| "" (SKOLEM-TYPEPRED) (("" (GROUND) NIL)))
(|fp_compare_TCC1| "" (TCC :DEFS !) NIL)
(|fp_compare_TCC2| "" (TCC :DEFS !) NIL)
(|posinf_ge| "" (SKOLEM-TYPEPRED)
(("" (PROP)
(("1" (EXPAND "pos")
(("1" (LEMMA "value_nonzero")
(("1" (INST?)
(("1" (HIDE 2)
(("1" (EXPAND "fp_compare")
(("1" (ASSERT)
(("1" (GROUND)
(("1" (LIFT-IF)
(("1" (EXPAND "n_value")
(("1" (REWRITE "expt_x0")
(("1" (GROUND)
(("1" (CASE "max_pos < b^(1+E_max)")
(("1"
(EXPAND "abs")
(("1" (LIFT-IF) (("1" (GROUND) NIL)))))
("2"
(HIDE -1 -2 -3 2)
(("2"
(LEMMA "max_fp_correct")
(("2"
(REPLACE -1)
(("2"
(ASSERT)
(("2"
(LEMMA "expt_pos")
(("2"
(INST-CP - "1+E_max" "b")
(("2"
(INST - "1+E_max-p" "b")
(("2"
(ASSERT)
NIL)))))))))))))))))))))))))
("2" (EXPAND "n_value")
(("2" (REWRITE "expt_x0")
(("2" (EXPAND "zero?")
(("2" (ASSERT)
(("2" (LEMMA "expt_pos")
(("2"
(INST?)
(("2"
(ASSERT)
NIL)))))))))))))))))))))))))))
("2" (EXPAND "pos")
(("2" (EXPAND "fp_compare")
(("2" (ASSERT)
(("2" (LIFT-IF)
(("2" (GROUND)
(("2" (HIDE -1 1 2 3)
(("2" (EXPAND "n_value")
(("2" (TYPEPRED "i_sign(num!1)")
(("2" (GROUND)
(("2" (REPLACE -1)
(("2" (REWRITE "expt_x0")
(("2" (REWRITE "expt_x1")
(("2"
(LEMMA "expt_pos")
(("2"
(INST?)
(("2"
(REWRITE
"both_sides_times_pos_gt1")
NIL)))))))))))))))))))))))))))))))))
(|NaN_unordered| "" (SKOSIMP*)
(("" (EXPAND "fp_compare")
(("" (ASSERT) (("" (LIFT-IF) (("" (GROUND) NIL)))))))))
(|eq_def| "" (SKOLEM-TYPEPRED)
(("" (EXPAND "eq?")
(("" (EXPAND "fp_compare")
(("" (LIFT-IF) (("" (GROUND) NIL)))))))))
(|ne_def| "" (SKOLEM-TYPEPRED)
(("" (EXPAND "ne?")
(("" (EXPAND "fp_compare")
(("" (LIFT-IF) (("" (GROUND) NIL)))))))))
(|gt_def| "" (SKOLEM-TYPEPRED)
(("" (EXPAND "gt?")
(("" (EXPAND "fp_compare")
(("" (LIFT-IF) (("" (GROUND) NIL)))))))))
(|ge_def| "" (SKOLEM-TYPEPRED)
(("" (EXPAND "ge?")
(("" (EXPAND "fp_compare")
(("" (LIFT-IF) (("" (GROUND) NIL)))))))))
(|lt_def| "" (SKOLEM-TYPEPRED)
(("" (EXPAND "lt?")
(("" (EXPAND "fp_compare")
(("" (LIFT-IF) (("" (GROUND) NIL)))))))))
(|le_def| "" (SKOLEM-TYPEPRED)
(("" (EXPAND "le?")
(("" (EXPAND "fp_compare")
(("" (LIFT-IF) (("" (GROUND) NIL)))))))))
(|un_def| "" (SKOSIMP*)
(("" (EXPAND "un?")
(("" (EXPAND "fp_compare")
(("" (LIFT-IF) (("" (GROUND) NIL))))))))))
$$$infinity_arithmetic.pvs
infinity_arithmetic
[b,p:above(1),
E_max:integer,
E_min:{i:integer|E_max>i}]: THEORY
BEGIN
IMPORTING IEEE_854_values[b,p,E_max,E_min],
enumerated_type_defs
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Special functions for handling arithmetic on infinities
% These definitions return an undetermined NaN when the Invalid
% exception should be raised.
%
% The definitions come from constraints enumerated in sections
% 6.1, 6.3, and 7.1 of IEEE-854
%
fp: var fp_num
num,num1,num2: var {fp| finite?(fp) or infinite?(fp)}
% Addition when at least one operand is an infinity
fp_add_inf(num1, (num2: {num | infinite?(num1) OR infinite?(num)})): fp_num
=
IF infinite?(num1) & infinite?(num2) THEN
IF (i_sign(num1) = i_sign(num2)) THEN num1
ELSE invalid
ENDIF
ELSIF infinite?(num1) THEN num1
ELSE num2
ENDIF
% Addition when at least one operand is an infinity with exceptions
fp_add_inf_x(num1, (num2: {num | infinite?(num1) OR infinite?(num)})):
[fp_num, exception]
=
IF infinite?(num1) & infinite?(num2) THEN
IF (i_sign(num1) = i_sign(num2)) THEN (num1,no_exceptions)
ELSE (invalid,invalid_operation)
ENDIF
ELSIF infinite?(num1) THEN (num1,no_exceptions)
ELSE (num2,no_exceptions)
ENDIF
% Similarly for subtraction
fp_sub_inf(num1, (num2: {num | infinite?(num1) OR infinite?(num)})): fp_num
=
IF infinite?(num1) & infinite?(num2) THEN
IF (i_sign(num1) /= i_sign(num2)) THEN num1
ELSE invalid
ENDIF
ELSIF infinite?(num1) THEN num1
ELSE toggle_sign(num2)
ENDIF
% Similarly for subtraction with exceptions
fp_sub_inf_x(num1, (num2: {num | infinite?(num1) OR infinite?(num)})):
[fp_num , exception]
=
IF infinite?(num1) & infinite?(num2) THEN
IF (i_sign(num1) /= i_sign(num2)) THEN (num1, no_exceptions)
ELSE (invalid, invalid_operation)
ENDIF
ELSIF infinite?(num1) THEN (num1, no_exceptions)
ELSE (toggle_sign(num2), no_exceptions)
ENDIF
% Alternate definition for fp_sub_inf
fp_sub_inf_def: lemma
forall num1,(num2:{num|infinite?(num1) OR infinite?(num)}):
fp_sub_inf(num1,num2) = fp_add_inf(num1,toggle_sign(num2));
% xor function defined on sign_rep to determine correct sign for mult/div
xor(s1,s2:sign_rep): sign_rep = if s1=s2 then 0 else 1 endif
% Determine correct sign for multiplication and division
% this definition is complicated by a bug in the adt mechanism
% PVS does not currently allow use of the same accessor for
% different constructors.
mult_sign(num1,num2):sign_rep =
if infinite?(num1) then
if infinite?(num2) then
xor(i_sign(num1),i_sign(num2))
else
xor(i_sign(num1),sign(num2))
endif
elsif infinite?(num2) then
xor(sign(num1),i_sign(num2))
else
xor(sign(num1),sign(num2))
endif
% Multiplication of infinity
% The use of mult_sign may be replaced by xor(sign(num1),sign(num2))
% as soon as the accessor bug is fixed.
fp_mul_inf(num1, (num2: {num | infinite?(num1) OR infinite?(num)})): fp_num
=
If zero?(num1) or zero?(num2) then invalid
else infinite(mult_sign(num1,num2))
endif
% Division with infinities
fp_div_inf(num1, (num2: {num | infinite?(num1) OR infinite?(num)})): fp_num
=
IF infinite?(num1) & infinite?(num2) THEN invalid
ELSIF infinite?(num1) THEN infinite(mult_sign(num1,num2))
ELSE finite(mult_sign(num1,num2),E_min,d_zero)
ENDIF
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
END infinity_arithmetic
$$$infinity_arithmetic.prf
(|infinity_arithmetic| (IMPORTING1_TCC1 "" (INST 1 "E_max - 1") NIL)
(|fp_add_inf_TCC1| "" (TCC :DEFS !) NIL)
(|fp_add_inf_TCC2| "" (TCC :DEFS !) NIL)
(|fp_sub_inf_def_TCC1| "" (SKOLEM-TYPEPRED)
(("" (REWRITE "toggle_infinite")
(("" (REWRITE "toggle_finite") (("" (GROUND) NIL)))))))
(|fp_sub_inf_def| "" (SKOSIMP*)
(("" (REWRITE "fp_sub_inf")
(("" (REWRITE "fp_add_inf")
(("1" (REWRITE "toggle_infinite")
(("1" (LIFT-IF)
(("1" (LIFT-IF)
(("1" (GROUND)
(("1" (EXPAND "toggle_sign") (("1" (ASSERT) NIL)))
("2" (EXPAND "toggle_sign")
(("2" (TYPEPRED "i_sign(num2!1)")
(("2" (TYPEPRED "i_sign(num1!1)")
(("2" (GROUND) NIL)))))))))))))))
("2" (REWRITE "toggle_infinite")
(("2" (REWRITE "toggle_finite")
(("2" (TYPEPRED "num2!1") (("2" (GROUND) NIL)))))))))))))
(XOR_TCC1 "" (TCC :DEFS !) NIL) (XOR_TCC2 "" (TCC :DEFS !) NIL)
(|mult_sign_TCC1| "" (SKOLEM-TYPEPRED) (("" (GROUND) NIL)))
(|mult_sign_TCC2| "" (SKOLEM-TYPEPRED) (("" (GROUND) NIL)))
(|mult_sign_TCC3| "" (SKOLEM-TYPEPRED) (("" (GROUND) NIL)))
(|mult_sign_TCC4| "" (SKOLEM-TYPEPRED) (("" (GROUND) NIL)))
(|fp_div_inf_TCC1| "" (SKOSIMP*) (("" (ASSERT) NIL))))
$$$NaN_ops.pvs
NaN_ops
[b,p:above(1),
E_max:integer,
E_min:{i:integer|E_max>i}]: THEORY
BEGIN
IMPORTING IEEE_854_values[b,p,E_max,E_min],
enumerated_type_defs
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Placeholders for defining results of operations on NaNs
fp,fp1,fp2: var fp_num
nan,nan1,nan2: var (NaN?)
op: var fp_ops
signal?(fp):bool = if NaN?(fp) then signal?(status(fp)) else false endif
% mk_quiet takes an fp_num and coerces all NaNs into quiet NaNs.
% all numeric floating-point arguments are left unchanged
mk_quiet(fp): fp_num = if NaN?(fp) then NaN(quiet,data(fp)) else fp endif
mk_quiet_correct: lemma not signal?(fp) => mk_quiet(fp) = fp
fp_quiet(op,fp1,(fp2| NaN?(fp1) OR NaN?(fp2))):{nan| nan=fp1 or nan=fp2}
fp_signal(op, fp1,(fp2| NaN?(fp1) OR NaN?(fp2))): fp_num =
IF trap_enabled?(invalid_operation) THEN invalid
ELSE fp_quiet(op, mk_quiet(fp1), mk_quiet(fp2))
ENDIF
fp_nan(op, fp1, (fp2| NaN?(fp1) OR NaN?(fp2))): fp_num =
IF signal?(fp1) OR signal?(fp2) THEN fp_signal(op, fp1, fp2)
ELSE fp_quiet(op, fp1, fp2)
ENDIF
NaN_ops_correct: LEMMA
NOT trap_enabled?(invalid_operation) & (NaN?(fp1) OR NaN?(fp2))
=> quiet?(status(fp_nan(op, fp1, fp2)))
fp_nan_x(op, fp1, (fp2| NaN?(fp1) OR NaN?(fp2))): [fp_num,exception] =
IF signal?(fp1) OR signal?(fp2) THEN
(fp_signal(op, fp1, fp2),invalid_operation)
ELSE
(fp_quiet(op, fp1, fp2), no_exceptions)
ENDIF
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
NaN_sqrt(nan): fp_num =
if signal?(status(nan))
& trap_enabled?(invalid_operation) then
invalid
else NaN(quiet,data(nan))
endif
END NaN_ops
$$$NaN_ops.prf
(|NaN_ops| (IMPORTING1_TCC1 "" (INST 1 "E_max - 1") NIL)
(|mk_quiet_correct| "" (GRIND)
(("" (LEMMA "fp_num_NaN_eta") (("" (INST?) (("" (ASSERT) NIL)))))))
(|fp_quiet_TCC1| ""
(INST +
"lambda op,fp1,(fp2|NaN?(fp1) or NaN?(fp2)): if NaN?(fp1) then fp1 else fp2 endif")
(("1" (SKOLEM-TYPEPRED) (("1" (PROP) NIL))) ("2" (SKOSIMP*) NIL)))
(|fp_signal_TCC1| "" (SKOLEM-TYPEPRED) (("" (GRIND) NIL)))
(|NaN_ops_correct_TCC1| "" (TCC :DEFS !) NIL)
(|NaN_ops_correct_TCC2| "" (TCC :DEFS !) NIL)
(|NaN_ops_correct| "" (SKOSIMP*)
(("" (EXPAND "fp_nan")
(("" (LIFT-IF)
(("" (EXPAND "fp_signal")
(("" (ASSERT)
(("" (SPLIT 2)
(("1" (FLATTEN)
(("1" (HIDE -1)
(("1"
(TYPEPRED
"fp_quiet(op!1, mk_quiet(fp1!1), mk_quiet(fp2!1))")
(("1" (GRIND) NIL) ("2" (GRIND) NIL)))))))
("2" (FLATTEN)
(("2" (TYPEPRED "fp_quiet(op!1, fp1!1, fp2!1)")
(("1" (EXPAND "signal?") (("1" (GRIND) NIL)))
("2" (PROPAX) NIL))))))))))))))))))
$$$sqrt.pvs
sqrt: THEORY
BEGIN
e: VAR posreal
x, y: VAR real
epsilon_delta: LEMMA (FORALL e: abs(x - y) < e) => x = y
px, py: VAR nonneg_real
times_pos_lt1: LEMMA px * py < 1 => px < 1 OR py < 1
times_pos_le1: LEMMA px * py <= 1 => px <= 1 OR py <= 1
times_pos_gt1: LEMMA px * py > 1 => px > 1 OR py > 1
times_pos_ge1: LEMMA px * py >= 1 => px >= 1 OR py >= 1
ge1_square_ge: LEMMA 1 <= px => px <= px * px
i: var posnat
expt_0: lemma 0^i = 0
ge1_expt_ge: LEMMA 1 <= px => px <= px ^ i
lt1_expt_le: LEMMA px<1 => px^i <= px
square_def: LEMMA x^2 = x*x
expt_pos_le: LEMMA px^i<=py^i <=> px<=py
expt_pos_lt: LEMMA px^i