%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 pxpy^i <=> px>py expt_pos_ge: LEMMA px^i>=py^i <=> px>=py sqrt(px): {py | py^2 = px} sqrt1: lemma sqrt(px^2)=px sqrt_abs: lemma sqrt(x^2) = abs(x) END sqrt $$$sqrt.prf (|sqrt| (|epsilon_delta| "" (SKOSIMP*) (("" (INST - "abs(x!1-y!1)/2") (("1" (ASSERT) NIL) ("2" (EXPAND "abs") (("2" (LIFT-IF) (("2" (GROUND) NIL))))))))) (|times_pos_lt1| "" (SKOSIMP*) (("" (LEMMA "ge_times_ge_pos") (("" (INST - "1" "1" "px!1" "py!1") (("" (GROUND) NIL))))))) (|times_pos_le1| "" (SKOSIMP*) (("" (LEMMA "gt_times_gt_pos1") (("" (INST - "1" "1" "px!1" "py!1") (("" (GROUND) NIL))))))) (|times_pos_gt1| "" (SKOSIMP*) (("" (LEMMA "le_times_le_pos") (("" (INST - "px!1" "py!1" "1" "1") (("" (ASSERT) NIL))))))) (|times_pos_ge1| "" (SKOSIMP*) (("" (LEMMA "lt_times_lt_pos1") (("" (INST - "px!1" "py!1" "1" "1") (("1" (ASSERT) NIL) ("2" (ASSERT) NIL))))))) (|ge1_square_ge| "" (SKOSIMP*) (("" (LEMMA "le_times_le_pos") (("" (INST - "1" "px!1" "px!1" "px!1") (("" (ASSERT) NIL))))))) (|expt_0| "" (TCC) NIL) (|ge1_expt_ge_TCC1| "" (TCC :DEFS !) NIL) (|ge1_expt_ge| "" (INDUCT "i" 1 "above_induction[0]") (("1" (ASSERT) NIL) ("2" (ASSERT) NIL) ("3" (SKOSIMP*) (("3" (REWRITE "expt_x1") (("3" (ASSERT) NIL))))) ("4" (SKOSIMP*) (("4" (REWRITE "expt_plus") (("4" (REWRITE "expt_x1") (("4" (ASSERT) (("4" (LEMMA "le_times_le_pos") (("4" (INST - "px!1" "1" "px!1" "px!1^ja!1") (("4" (ASSERT) (("4" (INST?) (("4" (ASSERT) NIL))))))))))))))))))) (|lt1_expt_le_TCC1| "" (TCC :DEFS !) NIL) (|lt1_expt_le| "" (INDUCT "i" 1 "above_induction[0]") (("1" (ASSERT) NIL) ("2" (ASSERT) NIL) ("3" (SKOSIMP*) (("3" (REWRITE "expt_x1") (("3" (ASSERT) NIL))))) ("4" (SKOSIMP*) (("4" (CASE "px!1=0") (("1" (REPLACE -1) (("1" (REWRITE "expt_0") (("1" (ASSERT) NIL))))) ("2" (REWRITE "expt_plus") (("2" (REWRITE "expt_x1") (("2" (ASSERT) (("2" (INST?) (("2" (ASSERT) (("2" (LEMMA "le_times_le_pos") (("2" (LEMMA "expt_pos") (("2" (INST?) (("2" (INST - "px!1^ja!1" "px!1" "1" "px!1") (("2" (ASSERT) NIL))))))))))))))))))))))))) (|square_def_TCC1| "" (TCC :DEFS !) NIL) (|square_def| "" (GRIND) NIL) (|expt_pos_le_TCC1| "" (TCC :DEFS !) NIL) (|expt_pos_le| "" (INDUCT "i" 1 "above_induction[0]") (("1" (ASSERT) NIL) ("2" (ASSERT) NIL) ("3" (SKOSIMP*) (("3" (REWRITE "expt_x1") (("3" (REWRITE "expt_x1") (("3" (ASSERT) NIL))))))) ("4" (SKOSIMP*) (("4" (ASSERT) (("4" (CASE "px!1 = 0") (("1" (REPLACE -1) (("1" (REWRITE "expt_0") (("1" (ASSERT) NIL))))) ("2" (CASE "py!1=0") (("1" (REPLACE -1) (("1" (REWRITE "expt_0") (("1" (ASSERT) (("1" (LEMMA "expt_pos") (("1" (INST?) (("1" (ASSERT) NIL))))))))))) ("2" (REWRITE "both_sides_expt_pos_le") NIL))))))))))) (|expt_pos_lt| "" (SKOSIMP*) (("" (LEMMA "expt_pos_le") (("" (INST - "i!1" "py!1" "px!1") (("" (GROUND) NIL))))))) (|expt_pos_gt| "" (SKOSIMP*) (("" (LEMMA "expt_pos_le") (("" (INST?) (("" (INST - "py!1") (("" (GROUND) NIL))))))))) (|expt_pos_ge| "" (SKOSIMP*) (("" (LEMMA "expt_pos_le") (("" (INST - "i!1" "py!1" "px!1") (("" (GROUND) NIL))))))) (|sqrt_TCC1| "" (TCC :DEFS !) NIL) (|sqrt_TCC2| "" (INST + "lambda px: choose({py|py^2=px})") (("" (SKOSIMP*) (("" (REWRITE "nonempty_exists") (("" (LEMMA "real_complete") (("" (INST - "{py|py^2<=px!1}") (("1" (PROP) (("1" (EXPAND "least_upper_bound?") (("1" (SKOSIMP*) (("1" (INST + "y!1") (("1" (EXPAND "upper_bound?") (("1" (ASSERT) (("1" (INST-CP - 0) (("1" (ASSERT) (("1" (CASE "forall (e:posreal|e