diff --git a/PVS_theories/double.pvs b/PVS_theories/double.pvs new file mode 100644 index 0000000000000000000000000000000000000000..ecf50379bb7dda5940f14e7552f71153697c5fe8 --- /dev/null +++ b/PVS_theories/double.pvs @@ -0,0 +1,10 @@ +double: THEORY + +BEGIN +IMPORTING float@enumerated_type_defs +IMPORTING overload[2,53,192,1023,-1022,to_nearest] + +double: TYPE = {fp:fp_num|finite?(fp) OR infinite?(fp)} +double_finite: TYPE = {fp:fp_num|finite?(fp)} + +END double diff --git a/PVS_theories/fp_lemmas.prf b/PVS_theories/fp_lemmas.prf new file mode 100644 index 0000000000000000000000000000000000000000..52d77a30757aa1491552ff15c76b9e2e62a0d680 --- /dev/null +++ b/PVS_theories/fp_lemmas.prf @@ -0,0 +1,870 @@ +(fp_lemmas + (infinite_not_zero 0 + (infinite_not_zero-1 nil 3508077004 3508077087 + ("" (skolem!) + (("" (expand zero?) + (("" (lift-if) + (("" (case "finite?[b, p, E_max, E_min](x!1)") + (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) + nil)) + nil)) + nil) + unchecked + ((zero? const-decl "bool" IEEE_854_values "float/") + (finite? adt-recognizer-decl "[fp_num -> boolean]" IEEE_854_values + "float/") + (fp_num type-decl nil IEEE_854_values "float/") + (E_min formal-const-decl "{i: integer | E_max > i}" fp_lemmas nil) + (E_max formal-const-decl "integer" fp_lemmas nil) + (integer nonempty-type-from-decl nil integers nil) + (p formal-const-decl "above(1)" fp_lemmas nil) + (b formal-const-decl "above(1)" fp_lemmas nil) + (above nonempty-type-eq-decl nil integers nil) + (> const-decl "bool" reals nil) + (bool nonempty-type-eq-decl nil booleans nil) + (int nonempty-type-eq-decl nil integers nil) + (integer_pred const-decl "[rational -> boolean]" integers nil) + (rational nonempty-type-from-decl nil rationals nil) + (rational_pred const-decl "[real -> boolean]" rationals nil) + (real nonempty-type-from-decl nil reals nil) + (real_pred const-decl "[number_field -> boolean]" reals nil) + (number_field nonempty-type-from-decl nil number_fields nil) + (number_field_pred const-decl "[number -> boolean]" number_fields + nil) + (boolean nonempty-type-decl nil booleans nil) + (number nonempty-type-decl nil numbers nil)) + 83425 30 t shostak)) + (op_fin_inf_TCC1 0 + (op_fin_inf_TCC1-1 nil 3508071655 nil ("" (subtype-tcc) nil nil) + unchecked nil nil nil nil nil)) + (op_fin_inf 0 + (op_fin_inf-1 nil 3508071661 3508071905 + ("" (skosimp) + (("" (expand fp_op) + (("" (assert) + (("" (case "fp_round(apply(op!1, x!1, y!1), mode!1) = 0") + (("1" (assert) nil nil) + ("2" (assert) + (("2" (expand real_to_fp) + (("2" + (case "abs(fp_round(apply(op!1, x!1, y!1), mode!1)) >= + b ^ (1 + E_max)") + (("1" (assert) nil nil) + ("2" (assert) + (("2" (lift-if) (("2" (assert) nil nil)) nil)) nil) + ("3" (assert) + (("3" (lemma Base_values) (("3" (assert) nil nil)) + nil)) + nil)) + nil)) + nil)) + nil) + ("3" (assert) + (("3" (lift-if) + (("3" (typepred "op!1") + (("3" (flatten) (("3" (assert) nil nil)) nil)) nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil) + unchecked + ((fp_op const-decl "fp_num" arithmetic_ops "float/") + (AND const-decl "[bool, bool -> bool]" booleans nil) + (OR const-decl "[bool, bool -> bool]" booleans nil) + (apply const-decl "real" arithmetic_ops "float/") + (zero? const-decl "bool" IEEE_854_values "float/") + (NOT const-decl "[bool -> bool]" booleans nil) + (div? adt-recognizer-decl "[fp_ops -> boolean]" + enumerated_type_defs "float/") + (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) + (finite? adt-recognizer-decl "[fp_num -> boolean]" IEEE_854_values + "float/") + (fp_num type-decl nil IEEE_854_values "float/") + (fp_ops type-decl nil enumerated_type_defs "float/") + (fp_round const-decl "real" real_to_fp "float/") + (E_min formal-const-decl "{i: integer | E_max > i}" fp_lemmas nil) + (E_max formal-const-decl "integer" fp_lemmas nil) + (alpha formal-const-decl "integer" fp_lemmas nil) + (integer nonempty-type-from-decl nil integers nil) + (p formal-const-decl "above(1)" fp_lemmas nil) + (b formal-const-decl "above(1)" fp_lemmas nil) + (above nonempty-type-eq-decl nil integers nil) + (> const-decl "bool" reals nil) + (bool nonempty-type-eq-decl nil booleans nil) + (int nonempty-type-eq-decl nil integers nil) + (integer_pred const-decl "[rational -> boolean]" integers nil) + (rational nonempty-type-from-decl nil rationals nil) + (rational_pred const-decl "[real -> boolean]" rationals nil) + (rounding_mode type-decl nil enumerated_type_defs "float/") + (real nonempty-type-from-decl nil reals nil) + (real_pred const-decl "[number_field -> boolean]" reals nil) + (number_field nonempty-type-from-decl nil number_fields nil) + (number_field_pred const-decl "[number -> boolean]" number_fields + nil) + (= const-decl "[T, T -> boolean]" equalities nil) + (boolean nonempty-type-decl nil booleans nil) + (number nonempty-type-decl nil numbers nil) + (real_to_fp const-decl "fp_num" real_to_fp "float/") + (real_lt_is_strict_total_order name-judgement + "(strict_total_order?[real])" real_props nil) + (posrat_exp application-judgement "posrat" exponentiation nil) + (nnrat_exp application-judgement "nnrat" exponentiation nil) + (real_ge_is_total_order name-judgement "(total_order?[real])" + real_props nil) + (int_plus_int_is_int application-judgement "int" integers nil) + (>= const-decl "bool" reals nil) + (nonneg_real nonempty-type-eq-decl nil real_types nil) + (numfield nonempty-type-eq-decl nil number_fields nil) + (- const-decl "[numfield -> numfield]" number_fields nil) + (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs + nil) + (/= const-decl "boolean" notequal nil) + (^ const-decl "real" exponentiation nil) + (+ const-decl "[numfield, numfield -> numfield]" number_fields + nil)) + 244314 320 t shostak)) + (op_add_inf_fin 0 + (op_add_inf_fin-1 nil 3508072296 3508072618 + ("" (skolem!) + (("" (expand XOR) + (("" (flatten) + (("" (assert) + (("" (lemma op_fin_inf) + (("" (inst?) + (("" (case "finite?(x!1)") + (("1" (assert) + (("1" (inst?) + (("1" (case "finite?(y!1)") + (("1" (assert) nil nil) + ("2" (assert) + (("2" (expand fp_add) + (("2" (assert) + (("2" (expand fp_add_inf) + (("2" (propax) nil nil)) nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil) + ("2" (assert) + (("2" (expand fp_add) + (("2" (lift-if) + (("2" (typepred "x!1") + (("2" (typepred "y!1") + (("2" (assert) + (("2" (case "finite?(y!1)") + (("1" + (assert) + (("1" + (expand fp_add_inf) + (("1" (propax) nil nil)) + nil)) + nil) + ("2" (assert) nil nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil) + unchecked + ((XOR const-decl "bool" xor_def nil) + (rounding_mode type-decl nil enumerated_type_defs "float/") + (NOT const-decl "[bool -> bool]" booleans nil) + (fp_add const-decl "fp_num" IEEE_854_defs "float/") + (fp_add_inf const-decl "fp_num" infinity_arithmetic "float/") + (number nonempty-type-decl nil numbers nil) + (boolean nonempty-type-decl nil booleans nil) + (number_field_pred const-decl "[number -> boolean]" number_fields + nil) + (number_field nonempty-type-from-decl nil number_fields nil) + (real_pred const-decl "[number_field -> boolean]" reals nil) + (real nonempty-type-from-decl nil reals nil) + (rational_pred const-decl "[real -> boolean]" rationals nil) + (rational nonempty-type-from-decl nil rationals nil) + (integer_pred const-decl "[rational -> boolean]" integers nil) + (int nonempty-type-eq-decl nil integers nil) + (bool nonempty-type-eq-decl nil booleans nil) + (> const-decl "bool" reals nil) + (above nonempty-type-eq-decl nil integers nil) + (b formal-const-decl "above(1)" fp_lemmas nil) + (p formal-const-decl "above(1)" fp_lemmas nil) + (integer nonempty-type-from-decl nil integers nil) + (E_max formal-const-decl "integer" fp_lemmas nil) + (E_min formal-const-decl "{i: integer | E_max > i}" fp_lemmas nil) + (fp_num type-decl nil IEEE_854_values "float/") + (finite? adt-recognizer-decl "[fp_num -> boolean]" IEEE_854_values + "float/") + (OR const-decl "[bool, bool -> bool]" booleans nil) + (infinite? adt-recognizer-decl "[fp_num -> boolean]" + IEEE_854_values "float/") + (op_fin_inf formula-decl nil fp_lemmas nil)) + 321637 560 t shostak)) + (op_add_inf_fin_l 0 + (op_add_inf_fin_l-1 nil 3508073321 3508073471 + ("" (skosimp) + (("" (expand fp_add) + (("" (case "finite?(x!1)") + (("1" (assert) + (("1" (lemma op_fin_inf) + (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) + nil) + ("2" (assert) + (("2" (lift-if) + (("2" (typepred x!1) + (("2" (assert) + (("2" (expand fp_add_inf) (("2" (propax) nil nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil) + unchecked + ((fp_add const-decl "fp_num" IEEE_854_defs "float/") + (fp_add_inf const-decl "fp_num" infinity_arithmetic "float/") + (rounding_mode type-decl nil enumerated_type_defs "float/") + (fp_ops type-decl nil enumerated_type_defs "float/") + (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) + (zero? const-decl "bool" IEEE_854_values "float/") + (AND const-decl "[bool, bool -> bool]" booleans nil) + (NOT const-decl "[bool -> bool]" booleans nil) + (div? adt-recognizer-decl "[fp_ops -> boolean]" + enumerated_type_defs "float/") + (add? adt-recognizer-decl "[fp_ops -> boolean]" + enumerated_type_defs "float/") + (add adt-constructor-decl "(add?)" enumerated_type_defs "float/") + (op_fin_inf formula-decl nil fp_lemmas nil) + (number nonempty-type-decl nil numbers nil) + (boolean nonempty-type-decl nil booleans nil) + (number_field_pred const-decl "[number -> boolean]" number_fields + nil) + (number_field nonempty-type-from-decl nil number_fields nil) + (real_pred const-decl "[number_field -> boolean]" reals nil) + (real nonempty-type-from-decl nil reals nil) + (rational_pred const-decl "[real -> boolean]" rationals nil) + (rational nonempty-type-from-decl nil rationals nil) + (integer_pred const-decl "[rational -> boolean]" integers nil) + (int nonempty-type-eq-decl nil integers nil) + (bool nonempty-type-eq-decl nil booleans nil) + (> const-decl "bool" reals nil) + (above nonempty-type-eq-decl nil integers nil) + (b formal-const-decl "above(1)" fp_lemmas nil) + (p formal-const-decl "above(1)" fp_lemmas nil) + (integer nonempty-type-from-decl nil integers nil) + (E_max formal-const-decl "integer" fp_lemmas nil) + (E_min formal-const-decl "{i: integer | E_max > i}" fp_lemmas nil) + (fp_num type-decl nil IEEE_854_values "float/") + (finite? adt-recognizer-decl "[fp_num -> boolean]" IEEE_854_values + "float/") + (OR const-decl "[bool, bool -> bool]" booleans nil) + (infinite? adt-recognizer-decl "[fp_num -> boolean]" + IEEE_854_values "float/")) + 150011 180 t shostak)) + (op_add_inf_fin_r 0 + (op_add_inf_fin_r-1 nil 3508073533 3508073612 + ("" (skosimp) + (("" (expand fp_add) + (("" (case "finite?(x!1)") + (("1" (assert) + (("1" (lemma op_fin_inf) + (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) + nil) + ("2" (assert) + (("2" (expand fp_add_inf) + (("2" (typepred "x!1") (("2" (assert) nil nil)) nil)) nil)) + nil)) + nil)) + nil)) + nil) + unchecked + ((fp_add const-decl "fp_num" IEEE_854_defs "float/") + (fp_add_inf const-decl "fp_num" infinity_arithmetic "float/") + (rounding_mode type-decl nil enumerated_type_defs "float/") + (fp_ops type-decl nil enumerated_type_defs "float/") + (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) + (zero? const-decl "bool" IEEE_854_values "float/") + (AND const-decl "[bool, bool -> bool]" booleans nil) + (NOT const-decl "[bool -> bool]" booleans nil) + (div? adt-recognizer-decl "[fp_ops -> boolean]" + enumerated_type_defs "float/") + (add? adt-recognizer-decl "[fp_ops -> boolean]" + enumerated_type_defs "float/") + (add adt-constructor-decl "(add?)" enumerated_type_defs "float/") + (op_fin_inf formula-decl nil fp_lemmas nil) + (number nonempty-type-decl nil numbers nil) + (boolean nonempty-type-decl nil booleans nil) + (number_field_pred const-decl "[number -> boolean]" number_fields + nil) + (number_field nonempty-type-from-decl nil number_fields nil) + (real_pred const-decl "[number_field -> boolean]" reals nil) + (real nonempty-type-from-decl nil reals nil) + (rational_pred const-decl "[real -> boolean]" rationals nil) + (rational nonempty-type-from-decl nil rationals nil) + (integer_pred const-decl "[rational -> boolean]" integers nil) + (int nonempty-type-eq-decl nil integers nil) + (bool nonempty-type-eq-decl nil booleans nil) + (> const-decl "bool" reals nil) + (above nonempty-type-eq-decl nil integers nil) + (b formal-const-decl "above(1)" fp_lemmas nil) + (p formal-const-decl "above(1)" fp_lemmas nil) + (integer nonempty-type-from-decl nil integers nil) + (E_max formal-const-decl "integer" fp_lemmas nil) + (E_min formal-const-decl "{i: integer | E_max > i}" fp_lemmas nil) + (fp_num type-decl nil IEEE_854_values "float/") + (finite? adt-recognizer-decl "[fp_num -> boolean]" IEEE_854_values + "float/") + (OR const-decl "[bool, bool -> bool]" booleans nil) + (infinite? adt-recognizer-decl "[fp_num -> boolean]" + IEEE_854_values "float/")) + 79167 80 t shostak)) + (op_sub_inf_fin_l 0 + (op_sub_inf_fin_l-1 nil 3508075475 3508075554 + ("" (skosimp) + (("" (expand fp_sub) + (("" (case "finite?(x!1)") + (("1" (assert) + (("1" (lemma op_fin_inf) + (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) + nil) + ("2" (assert) + (("2" (typepred "x!1") + (("2" (assert) + (("2" (expand fp_sub_inf) (("2" (propax) nil nil)) nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil) + unchecked + ((fp_sub const-decl "fp_num" IEEE_854_defs "float/") + (fp_sub_inf const-decl "fp_num" infinity_arithmetic "float/") + (rounding_mode type-decl nil enumerated_type_defs "float/") + (fp_ops type-decl nil enumerated_type_defs "float/") + (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) + (zero? const-decl "bool" IEEE_854_values "float/") + (AND const-decl "[bool, bool -> bool]" booleans nil) + (NOT const-decl "[bool -> bool]" booleans nil) + (div? adt-recognizer-decl "[fp_ops -> boolean]" + enumerated_type_defs "float/") + (sub? adt-recognizer-decl "[fp_ops -> boolean]" + enumerated_type_defs "float/") + (sub adt-constructor-decl "(sub?)" enumerated_type_defs "float/") + (op_fin_inf formula-decl nil fp_lemmas nil) + (number nonempty-type-decl nil numbers nil) + (boolean nonempty-type-decl nil booleans nil) + (number_field_pred const-decl "[number -> boolean]" number_fields + nil) + (number_field nonempty-type-from-decl nil number_fields nil) + (real_pred const-decl "[number_field -> boolean]" reals nil) + (real nonempty-type-from-decl nil reals nil) + (rational_pred const-decl "[real -> boolean]" rationals nil) + (rational nonempty-type-from-decl nil rationals nil) + (integer_pred const-decl "[rational -> boolean]" integers nil) + (int nonempty-type-eq-decl nil integers nil) + (bool nonempty-type-eq-decl nil booleans nil) + (> const-decl "bool" reals nil) + (above nonempty-type-eq-decl nil integers nil) + (b formal-const-decl "above(1)" fp_lemmas nil) + (p formal-const-decl "above(1)" fp_lemmas nil) + (integer nonempty-type-from-decl nil integers nil) + (E_max formal-const-decl "integer" fp_lemmas nil) + (E_min formal-const-decl "{i: integer | E_max > i}" fp_lemmas nil) + (fp_num type-decl nil IEEE_854_values "float/") + (finite? adt-recognizer-decl "[fp_num -> boolean]" IEEE_854_values + "float/") + (OR const-decl "[bool, bool -> bool]" booleans nil) + (infinite? adt-recognizer-decl "[fp_num -> boolean]" + IEEE_854_values "float/")) + 79640 100 t shostak)) + (op_sub_inf_fin_r 0 + (op_sub_inf_fin_r-1 nil 3508075559 3508075728 + ("" (skosimp) + (("" (expand fp_sub) + (("" (lift-if) + (("" (case "finite?(x!1)") + (("1" (assert) + (("1" (lemma "op_fin_inf") + (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) + nil) + ("2" (assert) + (("2" (typepred "x!1") + (("2" (assert) + (("2" (expand fp_sub_inf) + (("2" (assert) + (("2" (expand toggle_sign) (("2" (propax) nil nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil) + unchecked + ((fp_sub const-decl "fp_num" IEEE_854_defs "float/") + (infinite? adt-recognizer-decl "[fp_num -> boolean]" + IEEE_854_values "float/") + (OR const-decl "[bool, bool -> bool]" booleans nil) + (finite? adt-recognizer-decl "[fp_num -> boolean]" IEEE_854_values + "float/") + (fp_num type-decl nil IEEE_854_values "float/") + (E_min formal-const-decl "{i: integer | E_max > i}" fp_lemmas nil) + (E_max formal-const-decl "integer" fp_lemmas nil) + (integer nonempty-type-from-decl nil integers nil) + (p formal-const-decl "above(1)" fp_lemmas nil) + (b formal-const-decl "above(1)" fp_lemmas nil) + (above nonempty-type-eq-decl nil integers nil) + (> const-decl "bool" reals nil) + (bool nonempty-type-eq-decl nil booleans nil) + (int nonempty-type-eq-decl nil integers nil) + (integer_pred const-decl "[rational -> boolean]" integers nil) + (rational nonempty-type-from-decl nil rationals nil) + (rational_pred const-decl "[real -> boolean]" rationals nil) + (real nonempty-type-from-decl nil reals nil) + (real_pred const-decl "[number_field -> boolean]" reals nil) + (number_field nonempty-type-from-decl nil number_fields nil) + (number_field_pred const-decl "[number -> boolean]" number_fields + nil) + (boolean nonempty-type-decl nil booleans nil) + (number nonempty-type-decl nil numbers nil) + (op_fin_inf formula-decl nil fp_lemmas nil) + (sub adt-constructor-decl "(sub?)" enumerated_type_defs "float/") + (sub? adt-recognizer-decl "[fp_ops -> boolean]" + enumerated_type_defs "float/") + (div? adt-recognizer-decl "[fp_ops -> boolean]" + enumerated_type_defs "float/") + (NOT const-decl "[bool -> bool]" booleans nil) + (AND const-decl "[bool, bool -> bool]" booleans nil) + (zero? const-decl "bool" IEEE_854_values "float/") + (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) + (fp_ops type-decl nil enumerated_type_defs "float/") + (rounding_mode type-decl nil enumerated_type_defs "float/") + (fp_sub_inf const-decl "fp_num" infinity_arithmetic "float/") + (minus_odd_is_odd application-judgement "odd_int" integers nil) + (toggle_sign const-decl "fp_num" IEEE_854_values "float/")) + 168687 120 t shostak)) + (op_mul_inf_fin_l 0 + (op_mul_inf_fin_l-1 nil 3508077223 3508077459 + ("" (skosimp) + (("" (expand fp_mul) + (("" (lift-if) + (("" (case "finite?(x!1)") + (("1" (assert) + (("1" (lemma op_fin_inf) + (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) + nil) + ("2" (assert) + (("2" (typepred "x!1") + (("2" (assert) + (("2" (expand fp_mul_inf) + (("2" (lift-if) + (("2" (assert) + (("2" (typepred "x!1") + (("2" (assert) + (("2" (typepred "y!1") + (("2" (assert) + (("2" + (lemma infinite_not_zero) + (("2" + (assert) + (("2" + (inst -1 "x!1") + (("2" (assert) nil nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil) + unchecked + ((fp_mul const-decl "fp_num" IEEE_854_defs "float/") + (infinite? adt-recognizer-decl "[fp_num -> boolean]" + IEEE_854_values "float/") + (OR const-decl "[bool, bool -> bool]" booleans nil) + (finite? adt-recognizer-decl "[fp_num -> boolean]" IEEE_854_values + "float/") + (fp_num type-decl nil IEEE_854_values "float/") + (E_min formal-const-decl "{i: integer | E_max > i}" fp_lemmas nil) + (E_max formal-const-decl "integer" fp_lemmas nil) + (integer nonempty-type-from-decl nil integers nil) + (p formal-const-decl "above(1)" fp_lemmas nil) + (b formal-const-decl "above(1)" fp_lemmas nil) + (above nonempty-type-eq-decl nil integers nil) + (> const-decl "bool" reals nil) + (bool nonempty-type-eq-decl nil booleans nil) + (int nonempty-type-eq-decl nil integers nil) + (integer_pred const-decl "[rational -> boolean]" integers nil) + (rational nonempty-type-from-decl nil rationals nil) + (rational_pred const-decl "[real -> boolean]" rationals nil) + (real nonempty-type-from-decl nil reals nil) + (real_pred const-decl "[number_field -> boolean]" reals nil) + (number_field nonempty-type-from-decl nil number_fields nil) + (number_field_pred const-decl "[number -> boolean]" number_fields + nil) + (boolean nonempty-type-decl nil booleans nil) + (number nonempty-type-decl nil numbers nil) + (op_fin_inf formula-decl nil fp_lemmas nil) + (mult adt-constructor-decl "(mult?)" enumerated_type_defs "float/") + (mult? adt-recognizer-decl "[fp_ops -> boolean]" + enumerated_type_defs "float/") + (div? adt-recognizer-decl "[fp_ops -> boolean]" + enumerated_type_defs "float/") + (fp_ops type-decl nil enumerated_type_defs "float/") + (zero? const-decl "bool" IEEE_854_values "float/") + (NOT const-decl "[bool -> bool]" booleans nil) + (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) + (AND const-decl "[bool, bool -> bool]" booleans nil) + (rounding_mode type-decl nil enumerated_type_defs "float/") + (fp_mul_inf const-decl "fp_num" infinity_arithmetic "float/") + (infinite_not_zero formula-decl nil fp_lemmas nil)) + 235297 130 t shostak)) + (op_mul_inf_fin_r 0 + (op_mul_inf_fin_r-1 nil 3508076503 3508077221 + ("" (skosimp) + (("" (expand fp_mul) + (("" (lift-if) + (("" (case "finite?(x!1)") + (("1" (assert) + (("1" (lemma op_fin_inf) + (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) + nil) + ("2" (assert) + (("2" (typepred x!1) + (("2" (assert) + (("2" (expand fp_mul_inf) + (("2" (lift-if) + (("2" (typepred "y!1") + (("2" (simplify) + (("2" (lemma infinite_not_zero) + (("2" (inst -1 "x!1") + (("2" (assert) nil nil)) nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil) + unchecked + ((infinite_not_zero formula-decl nil fp_lemmas nil) + (fp_mul_inf const-decl "fp_num" infinity_arithmetic "float/") + (rounding_mode type-decl nil enumerated_type_defs "float/") + (AND const-decl "[bool, bool -> bool]" booleans nil) + (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) + (NOT const-decl "[bool -> bool]" booleans nil) + (zero? const-decl "bool" IEEE_854_values "float/") + (fp_ops type-decl nil enumerated_type_defs "float/") + (div? adt-recognizer-decl "[fp_ops -> boolean]" + enumerated_type_defs "float/") + (mult? adt-recognizer-decl "[fp_ops -> boolean]" + enumerated_type_defs "float/") + (mult adt-constructor-decl "(mult?)" enumerated_type_defs "float/") + (op_fin_inf formula-decl nil fp_lemmas nil) + (number nonempty-type-decl nil numbers nil) + (boolean nonempty-type-decl nil booleans nil) + (number_field_pred const-decl "[number -> boolean]" number_fields + nil) + (number_field nonempty-type-from-decl nil number_fields nil) + (real_pred const-decl "[number_field -> boolean]" reals nil) + (real nonempty-type-from-decl nil reals nil) + (rational_pred const-decl "[real -> boolean]" rationals nil) + (rational nonempty-type-from-decl nil rationals nil) + (integer_pred const-decl "[rational -> boolean]" integers nil) + (int nonempty-type-eq-decl nil integers nil) + (bool nonempty-type-eq-decl nil booleans nil) + (> const-decl "bool" reals nil) + (above nonempty-type-eq-decl nil integers nil) + (b formal-const-decl "above(1)" fp_lemmas nil) + (p formal-const-decl "above(1)" fp_lemmas nil) + (integer nonempty-type-from-decl nil integers nil) + (E_max formal-const-decl "integer" fp_lemmas nil) + (E_min formal-const-decl "{i: integer | E_max > i}" fp_lemmas nil) + (fp_num type-decl nil IEEE_854_values "float/") + (finite? adt-recognizer-decl "[fp_num -> boolean]" IEEE_854_values + "float/") + (OR const-decl "[bool, bool -> bool]" booleans nil) + (infinite? adt-recognizer-decl "[fp_num -> boolean]" + IEEE_854_values "float/") + (fp_mul const-decl "fp_num" IEEE_854_defs "float/")) + 342 100 t shostak)) + (op_div_inf_fin_l 0 + (op_div_inf_fin_l-1 nil 3508078503 3508078581 + ("" (skosimp) + (("" (expand fp_div) + (("" (case "finite?(x!1)") + (("1" (assert) + (("1" (lemma op_fin_inf) + (("1" (assert) (("1" (inst?) (("1" (assert) nil nil)) nil)) + nil)) + nil)) + nil) + ("2" (assert) + (("2" (typepred "x!1") + (("2" (assert) + (("2" (expand fp_div_inf) (("2" (propax) nil nil)) nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil) + unchecked + ((fp_div const-decl "fp_num" IEEE_854_defs "float/") + (fp_div_inf const-decl "fp_num" infinity_arithmetic "float/") + (div adt-constructor-decl "(div?)" enumerated_type_defs "float/") + (div? adt-recognizer-decl "[fp_ops -> boolean]" + enumerated_type_defs "float/") + (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) + (fp_ops type-decl nil enumerated_type_defs "float/") + (zero? const-decl "bool" IEEE_854_values "float/") + (NOT const-decl "[bool -> bool]" booleans nil) + (AND const-decl "[bool, bool -> bool]" booleans nil) + (rounding_mode type-decl nil enumerated_type_defs "float/") + (op_fin_inf formula-decl nil fp_lemmas nil) + (number nonempty-type-decl nil numbers nil) + (boolean nonempty-type-decl nil booleans nil) + (number_field_pred const-decl "[number -> boolean]" number_fields + nil) + (number_field nonempty-type-from-decl nil number_fields nil) + (real_pred const-decl "[number_field -> boolean]" reals nil) + (real nonempty-type-from-decl nil reals nil) + (rational_pred const-decl "[real -> boolean]" rationals nil) + (rational nonempty-type-from-decl nil rationals nil) + (integer_pred const-decl "[rational -> boolean]" integers nil) + (int nonempty-type-eq-decl nil integers nil) + (bool nonempty-type-eq-decl nil booleans nil) + (> const-decl "bool" reals nil) + (above nonempty-type-eq-decl nil integers nil) + (b formal-const-decl "above(1)" fp_lemmas nil) + (p formal-const-decl "above(1)" fp_lemmas nil) + (integer nonempty-type-from-decl nil integers nil) + (E_max formal-const-decl "integer" fp_lemmas nil) + (E_min formal-const-decl "{i: integer | E_max > i}" fp_lemmas nil) + (fp_num type-decl nil IEEE_854_values "float/") + (finite? adt-recognizer-decl "[fp_num -> boolean]" IEEE_854_values + "float/") + (OR const-decl "[bool, bool -> bool]" booleans nil) + (infinite? adt-recognizer-decl "[fp_num -> boolean]" + IEEE_854_values "float/")) + 78451 90 t shostak)) + (op_div_inf_fin_r 0 + (op_div_inf_fin_r-1 nil 3508078320 3508516292 + ("" (skolem!) + (("" (typepred y!1) + (("" (typepred x!1) + (("" (expand fp_div) + (("" (lift-if) + (("" (case "finite?(y!1)") + (("1" (assert) + (("1" (lemma "op_fin_inf") + (("1" (inst -1 "mode!1" "y!1" "x!1" "div") nil nil)) + nil)) + nil) + ("2" (assert) + (("2" (flatten) + (("2" (expand fp_div_inf) (("2" (propax) nil nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil) + proved + ((infinite? adt-recognizer-decl "[fp_num -> boolean]" + IEEE_854_values "float/") + (finite? adt-recognizer-decl "[fp_num -> boolean]" IEEE_854_values + "float/") + (fp_num type-decl nil IEEE_854_values "float/") + (E_min formal-const-decl "{i: integer | E_max > i}" fp_lemmas nil) + (E_max formal-const-decl "integer" fp_lemmas nil) + (integer nonempty-type-from-decl nil integers nil) + (p formal-const-decl "above(1)" fp_lemmas nil) + (b formal-const-decl "above(1)" fp_lemmas nil) + (above nonempty-type-eq-decl nil integers nil) + (> const-decl "bool" reals nil) + (int nonempty-type-eq-decl nil integers nil) + (integer_pred const-decl "[rational -> boolean]" integers nil) + (rational nonempty-type-from-decl nil rationals nil) + (rational_pred const-decl "[real -> boolean]" rationals nil) + (real nonempty-type-from-decl nil reals nil) + (real_pred const-decl "[number_field -> boolean]" reals nil) + (number_field nonempty-type-from-decl nil number_fields nil) + (number_field_pred const-decl "[number -> boolean]" number_fields + nil) + (number nonempty-type-decl nil numbers nil) + (OR const-decl "[bool, bool -> bool]" booleans nil) + (NOT const-decl "[bool -> bool]" booleans nil) + (bool nonempty-type-eq-decl nil booleans nil) + (boolean nonempty-type-decl nil booleans nil) + (fp_div const-decl "fp_num" IEEE_854_defs "float/") + (op_fin_inf formula-decl nil fp_lemmas nil) + (div adt-constructor-decl "(div?)" enumerated_type_defs "float/") + (div? adt-recognizer-decl "[fp_ops -> boolean]" + enumerated_type_defs "float/") + (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) + (fp_ops type-decl nil enumerated_type_defs "float/") + (rounding_mode type-decl nil enumerated_type_defs "float/") + (fp_div_inf const-decl "fp_num" infinity_arithmetic "float/") + (AND const-decl "[bool, bool -> bool]" booleans nil) + (zero? const-decl "bool" IEEE_854_values "float/")) + 139965 80 t shostak)) + (op_sqrt_inf_fin 0 + (op_sqrt_inf_fin-1 nil 3508077679 3508078174 + ("" (skosimp) + (("" (expand fp_sqrt) + (("" (lift-if) + (("" (assert) + (("" (typepred "x!1") + (("" (assert) + (("" (split) + (("1" (flatten) + (("1" (assert) + (("1" (case "zero?(x!1)") + (("1" (assert) nil nil) + ("2" (assert) + (("2" (expand real_to_fp) + (("2" + (case "abs(fp_round(sqrt(value(x!1)), mode!1)) >= b ^ (1 + E_max)") + (("1" (assert) nil nil) + ("2" (assert) + (("2" + (case + "abs(fp_round(sqrt(value(x!1)), mode!1)) < b ^ E_min") + (("1" (assert) nil nil) + ("2" (assert) nil nil)) + nil)) + nil) + ("3" (assert) (("3" (assert) nil nil)) + nil) + ("4" (assert) + (("4" + (hide 2 3 4) + (("4" + (lemma value_positive) + (("4" + (inst -1 "x!1") + (("4" (assert) nil nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil) + ("2" (flatten) (("2" (assert) nil nil)) nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil) + unchecked + ((fp_sqrt const-decl "fp_num" IEEE_854_defs "float/") + (zero? const-decl "bool" IEEE_854_values "float/") + (real_to_fp const-decl "fp_num" real_to_fp "float/") + (value_positive formula-decl nil IEEE_854_values "float/") + (real_gt_is_strict_total_order name-judgement + "(strict_total_order?[real])" real_props nil) + (real_lt_is_strict_total_order name-judgement + "(strict_total_order?[real])" real_props nil) + (nil name-judgement + "[integer, nonneg_real -> digits[b, p, E_max, E_min]]" fp_lemmas + nil) + (< const-decl "bool" reals nil) + (posrat_exp application-judgement "posrat" exponentiation nil) + (nnrat_exp application-judgement "nnrat" exponentiation nil) + (real_ge_is_total_order name-judgement "(total_order?[real])" + real_props nil) + (int_plus_int_is_int application-judgement "int" integers nil) + (nonneg_real nonempty-type-eq-decl nil real_types nil) + (numfield nonempty-type-eq-decl nil number_fields nil) + (- const-decl "[numfield -> numfield]" number_fields nil) + (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs + nil) + (rounding_mode type-decl nil enumerated_type_defs "float/") + (alpha formal-const-decl "integer" fp_lemmas nil) + (fp_round const-decl "real" real_to_fp "float/") + (* const-decl "[numfield, numfield -> numfield]" number_fields nil) + (sqrt const-decl "{nnz | nnz * nnz = nnx}" sqrt "reals/") + (value const-decl "real" IEEE_854_values "float/") + (/= const-decl "boolean" notequal nil) + (^ const-decl "real" exponentiation nil) + (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) + (boolean nonempty-type-decl nil booleans nil) + (bool nonempty-type-eq-decl nil booleans nil) + (NOT const-decl "[bool -> bool]" booleans nil) + (OR const-decl "[bool, bool -> bool]" booleans nil) + (AND const-decl "[bool, bool -> bool]" booleans nil) + (number nonempty-type-decl nil numbers nil) + (number_field_pred const-decl "[number -> boolean]" number_fields + nil) + (number_field nonempty-type-from-decl nil number_fields nil) + (real_pred const-decl "[number_field -> boolean]" reals nil) + (real nonempty-type-from-decl nil reals nil) + (rational_pred const-decl "[real -> boolean]" rationals nil) + (rational nonempty-type-from-decl nil rationals nil) + (integer_pred const-decl "[rational -> boolean]" integers nil) + (int nonempty-type-eq-decl nil integers nil) + (> const-decl "bool" reals nil) + (above nonempty-type-eq-decl nil integers nil) + (b formal-const-decl "above(1)" fp_lemmas nil) + (p formal-const-decl "above(1)" fp_lemmas nil) + (integer nonempty-type-from-decl nil integers nil) + (E_max formal-const-decl "integer" fp_lemmas nil) + (E_min formal-const-decl "{i: integer | E_max > i}" fp_lemmas nil) + (fp_num type-decl nil IEEE_854_values "float/") + (finite? adt-recognizer-decl "[fp_num -> boolean]" IEEE_854_values + "float/") + (= const-decl "[T, T -> boolean]" equalities nil) + (>= const-decl "bool" reals nil) + (nat nonempty-type-eq-decl nil naturalnumbers nil) + (sign_rep type-eq-decl nil enumerated_type_defs "float/") + (sign adt-accessor-decl "[(finite?) -> sign_rep]" IEEE_854_values + "float/") + (pos const-decl "sign_rep" enumerated_type_defs "float/") + (infinite? adt-recognizer-decl "[fp_num -> boolean]" + IEEE_854_values "float/") + (i_sign adt-accessor-decl "[(infinite?) -> sign_rep]" + IEEE_854_values "float/")) + 494694 470 t shostak))) + diff --git a/PVS_theories/fp_lemmas.pvs b/PVS_theories/fp_lemmas.pvs new file mode 100644 index 0000000000000000000000000000000000000000..2c7edfdb61494cac7125d453a1d162e839c4ae07 --- /dev/null +++ b/PVS_theories/fp_lemmas.pvs @@ -0,0 +1,39 @@ +fp_lemmas + [b,p:above(1), + alpha,E_max:integer, + E_min:{i:integer|E_max>i}]:THEORY + +BEGIN + + +IMPORTING float@IEEE_854_defs[b,p,alpha,E_max,E_min] + +infinite_not_zero: LEMMA FORALL (x:fp_num): infinite?(x) => NOT zero?(x) + +%finite_mul_1: LEMMA FORALL(x:{fp:fp_num|finite?(fp)},mode:rounding_mode): finite?(fp_mul(x,real_to_fp(1),mode)) + +op_fin_inf: LEMMA FORALL (mode:rounding_mode, x:{fp:fp_num|finite?(fp)}, y:{fp:fp_num| finite?(fp)},op:{op:fp_ops|zero?(y) OR (zero?(x) AND zero?(y)) => NOT div?(op)}): +finite?(fp_op(op,x,y,mode)) OR infinite?(fp_op(op,x,y,mode)) + +op_add_inf_fin: LEMMA FORALL (mode:rounding_mode, x:{fp:fp_num|finite?(fp) OR infinite?(fp)},y:{fp:fp_num| finite?(fp) OR infinite?(fp)}): infinite?(x) XOR infinite?(y) => finite?(fp_add(x,y,mode)) OR infinite?(fp_add(x,y,mode)) + +op_add_inf_fin_l: LEMMA FORALL (mode:rounding_mode, x:{fp:fp_num|finite?(fp) OR infinite?(fp)},y:{fp:fp_num| finite?(fp)}): finite?(fp_add(x,y,mode)) OR infinite?(fp_add(x,y,mode)) + +op_add_inf_fin_r: LEMMA FORALL (mode:rounding_mode, x:{fp:fp_num|finite?(fp) OR infinite?(fp)},y:{fp:fp_num| finite?(fp)}): finite?(fp_add(y,x,mode)) OR infinite?(fp_add(y,x,mode)) + +op_sub_inf_fin_l: LEMMA FORALL (mode:rounding_mode, x:{fp:fp_num|finite?(fp) OR infinite?(fp)},y:{fp:fp_num| finite?(fp)}): finite?(fp_sub(x,y,mode)) OR infinite?(fp_sub(x,y,mode)) + +op_sub_inf_fin_r: LEMMA FORALL (mode:rounding_mode, x:{fp:fp_num|finite?(fp) OR infinite?(fp)},y:{fp:fp_num| finite?(fp)}): finite?(fp_sub(y,x,mode)) OR infinite?(fp_sub(y,x,mode)) + +op_mul_inf_fin_l: LEMMA FORALL (mode:rounding_mode, x:{fp:fp_num|finite?(fp) OR infinite?(fp)},y:{fp:fp_num| finite?(fp) AND (infinite?(x) => NOT zero?(fp))}): finite?(fp_mul(y,x,mode)) OR infinite?(fp_mul(y,x,mode)) + +op_mul_inf_fin_r: LEMMA FORALL (mode:rounding_mode, x:{fp:fp_num|finite?(fp) OR infinite?(fp)},y:{fp:fp_num| finite?(fp) AND (infinite?(x) => NOT zero?(fp))}): finite?(fp_mul(x,y,mode)) OR infinite?(fp_mul(x,y,mode)) + +op_div_inf_fin_l: LEMMA FORALL (mode:rounding_mode, x:{fp:fp_num|finite?(fp) OR infinite?(fp)},y:{fp:fp_num| finite?(fp) AND NOT zero?(fp)}): finite?(fp_div(x,y,mode)) OR infinite?(fp_div(x,y,mode)) + +op_div_inf_fin_r: LEMMA FORALL (mode:rounding_mode, x:{fp:fp_num|finite?(fp) AND NOT zero?(fp)},y:{fp:fp_num| finite?(fp) OR infinite?(fp)}): finite?(fp_div(y,x,mode)) OR infinite?(fp_div(y,x,mode)) + +op_sqrt_inf_fin: LEMMA FORALL (mode:rounding_mode, x:{fp:fp_num|(finite?(fp) AND sign(fp) = pos) OR (infinite?(fp) AND i_sign(fp) = pos)}): finite?(fp_sqrt(x,mode)) OR infinite?(fp_sqrt(x,mode)) + + +END fp_lemmas diff --git a/PVS_theories/overload.prf b/PVS_theories/overload.prf new file mode 100644 index 0000000000000000000000000000000000000000..cbe44f902c93a49f8309971a13d93f1c8a6b1707 --- /dev/null +++ b/PVS_theories/overload.prf @@ -0,0 +1,93 @@ +(overload + (lessp_TCC1 0 + (lessp_TCC1-1 nil 3508513172 3508513284 + ("" (skolem!) (("" (grind) nil nil)) nil) proved + ((posrat_exp application-judgement "posrat" exponentiation nil) + (nnrat_exp application-judgement "nnrat" exponentiation nil) + (minus_odd_is_odd application-judgement "odd_int" integers nil) + (minus_real_is_real application-judgement "real" reals nil) + (real_to_fp const-decl "fp_num" real_to_fp "float/") + (number nonempty-type-decl nil numbers nil) + (boolean nonempty-type-decl nil booleans nil) + (number_field_pred const-decl "[number -> boolean]" number_fields + nil) + (numfield nonempty-type-eq-decl nil number_fields nil) + (- const-decl "[numfield -> numfield]" number_fields nil) + (sign_of const-decl "sign_rep" fp_round_aux "float/") + (pos const-decl "sign_rep" enumerated_type_defs "float/") + (neg const-decl "sign_rep" enumerated_type_defs "float/") + (^ const-decl "real" exponentiation nil) + (expt def-decl "real" exponentiation nil) + (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs + nil) + (real_ge_is_total_order name-judgement "(total_order?[real])" + real_props nil) + (real_lt_is_strict_total_order name-judgement + "(strict_total_order?[real])" real_props nil) + (posint_exp application-judgement "posint" exponentiation nil) + (posint_plus_nnint_is_posint application-judgement "posint" + integers nil) + (odd_plus_odd_is_even application-judgement "even_int" integers + nil) + (posnat_expt application-judgement "posnat" exponentiation nil) + (posrat_div_posrat_is_posrat application-judgement "posrat" + rationals nil) + (posint_times_posint_is_posint application-judgement "posint" + integers nil) + (even_times_int_is_even application-judgement "even_int" integers + nil) + (mult_divides1 application-judgement "(divides(n))" divides nil) + (mult_divides2 application-judgement "(divides(m))" divides nil) + (even_minus_odd_is_odd application-judgement "odd_int" integers + nil) + (odd_minus_odd_is_even application-judgement "even_int" integers + nil) + (minus_nzint_is_nzint application-judgement "nzint" integers nil) + (minus_even_is_even application-judgement "even_int" integers nil)) + 18355 5670 t nil)) + (expt_TCC1 0 + (expt_TCC1-1 nil 3508513172 3508513172 ("" (subtype-tcc) nil nil) + proved + ((boolean nonempty-type-decl nil booleans nil) + (bool nonempty-type-eq-decl nil booleans nil) + (NOT const-decl "[bool -> bool]" booleans nil) + (number nonempty-type-decl nil numbers nil) + (number_field_pred const-decl "[number -> boolean]" number_fields + nil) + (number_field nonempty-type-from-decl nil number_fields nil) + (real_pred const-decl "[number_field -> boolean]" reals nil) + (real nonempty-type-from-decl nil reals nil) + (>= const-decl "bool" reals nil) + (rational_pred const-decl "[real -> boolean]" rationals nil) + (rational nonempty-type-from-decl nil rationals nil) + (integer_pred const-decl "[rational -> boolean]" integers nil) + (int nonempty-type-eq-decl nil integers nil) + (nat nonempty-type-eq-decl nil naturalnumbers nil) + (int_minus_int_is_int application-judgement "int" integers nil) + (real_ge_is_total_order name-judgement "(total_order?[real])" + real_props nil)) + 17 20 nil nil)) + (expt_TCC2 0 + (expt_TCC2-1 nil 3508513172 3508513172 ("" (termination-tcc) nil nil) + proved nil 6 0 nil nil)) + (caret_TCC1 0 + (caret_TCC1-1 nil 3508513172 3508513172 ("" (subtype-tcc) nil nil) + proved + ((boolean nonempty-type-decl nil booleans nil) + (bool nonempty-type-eq-decl nil booleans nil) + (NOT const-decl "[bool -> bool]" booleans nil) + (number nonempty-type-decl nil numbers nil) + (number_field_pred const-decl "[number -> boolean]" number_fields + nil) + (number_field nonempty-type-from-decl nil number_fields nil) + (real_pred const-decl "[number_field -> boolean]" reals nil) + (real nonempty-type-from-decl nil reals nil) + (rational_pred const-decl "[real -> boolean]" rationals nil) + (rational nonempty-type-from-decl nil rationals nil) + (integer_pred const-decl "[rational -> boolean]" integers nil) + (int nonempty-type-eq-decl nil integers nil) + (minus_int_is_int application-judgement "int" integers nil) + (real_ge_is_total_order name-judgement "(total_order?[real])" + real_props nil)) + 16 20 nil nil))) + diff --git a/PVS_theories/overload.pvs b/PVS_theories/overload.pvs new file mode 100644 index 0000000000000000000000000000000000000000..2339c3927022fa5e5e364acb199e6a88a0c296eb --- /dev/null +++ b/PVS_theories/overload.pvs @@ -0,0 +1,60 @@ +overload[b,p:above(1), + alpha,E_max:integer, + E_min:{i:integer|E_max>i}, +(IMPORTING float@enumerated_type_defs)r_mode:rounding_mode]:THEORY + +BEGIN + +IMPORTING fp_lemmas[b,p,alpha,E_max,E_min] + +x,y: VAR fp_num +n:VAR nat + +-(x,y):fp_num = fp_sub(x,y,r_mode); ++(x,y):fp_num = fp_add(x,y,r_mode); +*(x,y):fp_num = fp_mul(x,y,r_mode); +/(x,y):fp_num = fp_div(x,y,r_mode); +sqrt(x):fp_num = fp_sqrt(x,r_mode); +-(x):fp_num = toggle_sign(x); + +-(x:fp_num,y:real):fp_num = x-real_to_fp(y); ++(x:fp_num,y:real):fp_num = x+real_to_fp(y); +*(x:fp_num,y:real):fp_num = x*real_to_fp(y); +/(x:fp_num,y:real):fp_num = x/real_to_fp(y); + +-(x:real,y:fp_num):fp_num = real_to_fp(x)-y; ++(x:real,y:fp_num):fp_num = real_to_fp(x)+y; +*(x:real,y:fp_num):fp_num = real_to_fp(x)*y; +/(x:real,y:fp_num):fp_num = real_to_fp(x)/y; + + +<(x,y:{fp:fp_num|finite?(fp) OR infinite?(fp)}):bool = n_value(x) < n_value(y); +<=(x,y:{fp:fp_num|finite?(fp) OR infinite?(fp)}):bool = n_value(x) <= n_value(y); +>(x,y:{fp:fp_num|finite?(fp) OR infinite?(fp)}):bool = n_value(x) > n_value(y); +>=(x,y:{fp:fp_num|finite?(fp) OR infinite?(fp)}):bool = n_value(x) >= n_value(y); +=(x,y:{fp:fp_num|finite?(fp) OR infinite?(fp)}):bool = n_value(x) = n_value(y); +/=(x,y:{fp:fp_num|finite?(fp) OR infinite?(fp)}):bool = n_value(x) /= n_value(y); + +<(x:real,y:{fp:fp_num|finite?(fp) OR infinite?(fp)}):bool = real_to_fp(x) < y; +<=(x:real,y:{fp:fp_num|finite?(fp) OR infinite?(fp)}):bool = real_to_fp(x) <= y; +>(x:real,y:{fp:fp_num|finite?(fp) OR infinite?(fp)}):bool = real_to_fp(x) > y; +>=(x:real,y:{fp:fp_num|finite?(fp) OR infinite?(fp)}):bool = real_to_fp(x) >= y; +=(x:real,y:{fp:fp_num|finite?(fp) OR infinite?(fp)}):bool = real_to_fp(x) = y; +/=(x:real,y:{fp:fp_num|finite?(fp) OR infinite?(fp)}):bool = real_to_fp(x) /= y; + +<(x:{fp:fp_num|finite?(fp) OR infinite?(fp)},y:real):bool = x < real_to_fp(y); +<=(x:{fp:fp_num|finite?(fp) OR infinite?(fp)},y:real):bool = x <= real_to_fp(y); +>(x:{fp:fp_num|finite?(fp) OR infinite?(fp)},y:real):bool = x > real_to_fp(y); +>=(x:{fp:fp_num|finite?(fp) OR infinite?(fp)},y:real):bool = x >= real_to_fp(y); +=(x:{fp:fp_num|finite?(fp) OR infinite?(fp)},y:real):bool = x = real_to_fp(y); +/=(x:{fp:fp_num|finite?(fp) OR infinite?(fp)},y:real):bool = x /= real_to_fp(y); + +expt(x,n): RECURSIVE fp_num = + IF n = 0 THEN real_to_fp(1) + ELSE x * expt(x, n-1) + ENDIF +MEASURE n; + +^(x: fp_num, i:int): fp_num + = IF i >= 0 THEN expt(x, i) ELSE real_to_fp(1)/expt(x, -i) ENDIF +END overload diff --git a/PVS_theories/single.pvs b/PVS_theories/single.pvs new file mode 100644 index 0000000000000000000000000000000000000000..15248f798314493cb8b6b57289330d61e36d2c7e --- /dev/null +++ b/PVS_theories/single.pvs @@ -0,0 +1,11 @@ +single: THEORY + +BEGIN + +IMPORTING float@enumerated_type_defs +IMPORTING overload[2,24,192,127,-126,to_nearest] + +single: TYPE = {fp:fp_num|finite?(fp) OR infinite?(fp)} +single_finite: TYPE = {fp:fp_num|finite?(fp)} + +END single