diff --git a/thys/IEEE_Floating_Point/IEEE.thy b/thys/IEEE_Floating_Point/IEEE.thy --- a/thys/IEEE_Floating_Point/IEEE.thy +++ b/thys/IEEE_Floating_Point/IEEE.thy @@ -1,475 +1,475 @@ (* Formalization of IEEE-754 Standard for binary floating-point arithmetic *) (* Author: Lei Yu, University of Cambridge Contrib: Peter Lammich: fixed wrong sign handling in fmadd *) section \Specification of the IEEE standard\ theory IEEE imports "HOL-Library.Float" Word_Lib.Word_Lemmas begin typedef (overloaded) ('e::len, 'f::len) float = "UNIV::(1 word \ 'e word \ 'f word) set" by auto setup_lifting type_definition_float syntax "_float" :: "type \ type \ type" ("'(_, _') float") text \parse \('a, 'b) float\ as ('a::len, 'b::len) float.\ parse_translation \ let fun float t u = Syntax.const @{type_syntax float} $ t $ u; fun len_tr u = (case Term_Position.strip_positions u of v as Free (x, _) => if Lexicon.is_tid x then (Syntax.const @{syntax_const "_ofsort"} $ v $ Syntax.const @{class_syntax len}) else u | _ => u) fun len_float_tr [t, u] = float (len_tr t) (len_tr u) in [(@{syntax_const "_float"}, K len_float_tr)] end \ subsection \Derived parameters for floating point formats\ definition wordlength :: "('e, 'f) float itself \ nat" where "wordlength x = LENGTH('e) + LENGTH('f) + 1" definition bias :: "('e, 'f) float itself \ nat" where "bias x = 2^(LENGTH('e) - 1) - 1" definition emax :: "('e, 'f) float itself \ nat" where "emax x = unat (- 1::'e word)" abbreviation fracwidth::"('e, 'f) float itself \ nat" where "fracwidth _ \ LENGTH('f)" subsection \Predicates for the four IEEE formats\ definition is_single :: "('e, 'f) float itself \ bool" where "is_single x \ LENGTH('e) = 8 \ wordlength x = 32" definition is_double :: "('e, 'f) float itself \ bool" where "is_double x \ LENGTH('e) = 11 \ wordlength x = 64" definition is_single_extended :: "('e, 'f) float itself \ bool" where "is_single_extended x \ LENGTH('e) \ 11 \ wordlength x \ 43" definition is_double_extended :: "('e, 'f) float itself \ bool" where "is_double_extended x \ LENGTH('e) \ 15 \ wordlength x \ 79" subsection \Extractors for fields\ lift_definition sign::"('e, 'f) float \ nat" is "\(s::1 word, _::'e word, _::'f word). unat s" . lift_definition exponent::"('e, 'f) float \ nat" is "\(_, e::'e word, _). unat e" . lift_definition fraction::"('e, 'f) float \ nat" is "\(_, _, f::'f word). unat f" . abbreviation "real_of_word x \ real (unat x)" lift_definition valof :: "('e, 'f) float \ real" is "\(s, e, f). let x = (TYPE(('e, 'f) float)) in (if e = 0 then (-1::real)^(unat s) * (2 / (2^bias x)) * (real_of_word f/2^(LENGTH('f))) else (-1::real)^(unat s) * ((2^(unat e)) / (2^bias x)) * (1 + real_of_word f/2^LENGTH('f)))" . subsection \Partition of numbers into disjoint classes\ definition is_nan :: "('e, 'f) float \ bool" where "is_nan a \ exponent a = emax TYPE(('e, 'f)float) \ fraction a \ 0" definition is_infinity :: "('e, 'f) float \ bool" where "is_infinity a \ exponent a = emax TYPE(('e, 'f)float) \ fraction a = 0" definition is_normal :: "('e, 'f) float \ bool" where "is_normal a \ 0 < exponent a \ exponent a < emax TYPE(('e, 'f)float)" definition is_denormal :: "('e, 'f) float \ bool" where "is_denormal a \ exponent a = 0 \ fraction a \ 0" definition is_zero :: "('e, 'f) float \ bool" where "is_zero a \ exponent a = 0 \ fraction a = 0" definition is_finite :: "('e, 'f) float \ bool" where "is_finite a \ (is_normal a \ is_denormal a \ is_zero a)" subsection \Special values\ lift_definition plus_infinity :: "('e, 'f) float" ("\") is "(0, - 1, 0)" . lift_definition topfloat :: "('e, 'f) float" is "(0, - 2, 2^LENGTH('f) - 1)" . instantiation float::(len, len) zero begin lift_definition zero_float :: "('e, 'f) float" is "(0, 0, 0)" . instance proof qed end subsection \Negation operation on floating point values\ instantiation float::(len, len) uminus begin lift_definition uminus_float :: "('e, 'f) float \ ('e, 'f) float" is "\(s, e, f). (1 - s, e, f)" . instance proof qed end abbreviation (input) "minus_zero \ - (0::('e, 'f)float)" abbreviation (input) "minus_infinity \ - \" abbreviation (input) "bottomfloat \ - topfloat" subsection \Real number valuations\ text \The largest value that can be represented in floating point format.\ definition largest :: "('e, 'f) float itself \ real" where "largest x = (2^(emax x - 1) / 2^bias x) * (2 - 1/(2^fracwidth x))" text \Threshold, used for checking overflow.\ definition threshold :: "('e, 'f) float itself \ real" where "threshold x = (2^(emax x - 1) / 2^bias x) * (2 - 1/(2^(Suc(fracwidth x))))" text \Unit of least precision.\ lift_definition one_lp::"('e ,'f) float \ ('e ,'f) float" is "\(s, e, f). (0, e::'e word, 1)" . lift_definition zero_lp::"('e ,'f) float \ ('e ,'f) float" is "\(s, e, f). (0, e::'e word, 0)" . definition ulp :: "('e, 'f) float \ real" where "ulp a = valof (one_lp a) - valof (zero_lp a)" text \Enumerated type for rounding modes.\ datatype roundmode = roundNearestTiesToEven | roundNearestTiesToAway | roundTowardPositive | roundTowardNegative | roundTowardZero abbreviation (input) "RNE \ roundNearestTiesToEven" abbreviation (input) "RNA \ roundNearestTiesToAway" abbreviation (input) "RTP \ roundTowardPositive" abbreviation (input) "RTN \ roundTowardNegative" -abbreviation (input) "RNZ \ roundTowardZero" +abbreviation (input) "RTZ \ roundTowardZero" subsection \Rounding\ text \Characterization of best approximation from a set of abstract values.\ definition "is_closest v s x a \ a \ s \ (\b. b \ s \ \v a - x\ \ \v b - x\)" text \Best approximation with a deciding preference for multiple possibilities.\ definition "closest v p s x = (SOME a. is_closest v s x a \ ((\b. is_closest v s x b \ p b) \ p a))" fun round :: "roundmode \ real \ ('e ,'f) float" where "round roundNearestTiesToEven y = (if y \ - threshold TYPE(('e ,'f) float) then minus_infinity else if y \ threshold TYPE(('e ,'f) float) then plus_infinity else closest (valof) (\a. even (fraction a)) {a. is_finite a} y)" (*FIXME: broken, especially if both nearest are odd*) | "round roundNearestTiesToAway y = (if y \ - threshold TYPE(('e ,'f) float) then minus_infinity else if y \ threshold TYPE(('e ,'f) float) then plus_infinity else closest (valof) (\a. True) {a. is_finite a \ \valof a\ \ \y\} y)" | "round roundTowardPositive y = (if y < - largest TYPE(('e ,'f) float) then bottomfloat else if y > largest TYPE(('e ,'f) float) then plus_infinity else closest (valof) (\a. True) {a. is_finite a \ valof a \ y} y)" | "round roundTowardNegative y = (if y < - largest TYPE(('e ,'f) float) then minus_infinity else if y > largest TYPE(('e ,'f) float) then topfloat else closest (valof) (\a. True) {a. is_finite a \ valof a \ y} y)" | "round roundTowardZero y = (if y < - largest TYPE(('e ,'f) float) then bottomfloat else if y > largest TYPE(('e ,'f) float) then topfloat else closest (valof) (\a. True) {a. is_finite a \ \valof a\ \ \y\} y)" text \Rounding to integer values in floating point format.\ definition is_integral :: "('e ,'f) float \ bool" where "is_integral a \ is_finite a \ (\n::nat. \valof a\ = real n)" fun intround :: "roundmode \ real \ ('e ,'f) float" where "intround roundNearestTiesToEven y = (if y \ - threshold TYPE(('e ,'f) float) then minus_infinity else if y \ threshold TYPE(('e ,'f) float) then plus_infinity else closest (valof) (\a. (\n::nat. even n \ \valof a\ = real n)) {a. is_integral a} y)" | "intround roundNearestTiesToAway y = (if y \ - threshold TYPE(('e ,'f) float) then minus_infinity else if y \ threshold TYPE(('e ,'f) float) then plus_infinity else closest (valof) (\x. True) {a. is_integral a \ \valof a\ \ \y\} y)" | "intround roundTowardPositive y = (if y < - largest TYPE(('e ,'f) float) then bottomfloat else if y > largest TYPE(('e ,'f) float) then plus_infinity else closest (valof) (\x. True) {a. is_integral a \ valof a \ y} y)" | "intround roundTowardNegative y = (if y < - largest TYPE(('e ,'f) float) then minus_infinity else if y > largest TYPE(('e ,'f) float) then topfloat else closest (valof) (\x. True) {a. is_integral a \ valof a \ y} y)" | "intround roundTowardZero y = (if y < - largest TYPE(('e ,'f) float) then bottomfloat else if y > largest TYPE(('e ,'f) float) then topfloat else closest (valof) (\x. True) {a. is_integral a \ \valof a\ \ \y\} y)" text \Round, choosing between -0.0 or +0.0\ definition float_round::"roundmode \ bool \ real \ ('e, 'f) float" where "float_round mode toneg r = (let x = round mode r in if is_zero x then if toneg then minus_zero else 0 else x)" text \Non-standard of NaN.\ definition some_nan :: "('e ,'f) float" where "some_nan = (SOME a. is_nan a)" text \Coercion for signs of zero results.\ definition zerosign :: "nat \ ('e ,'f) float \ ('e ,'f) float" where "zerosign s a = (if is_zero a then (if s = 0 then 0 else - 0) else a)" text \Remainder operation.\ definition rem :: "real \ real \ real" where "rem x y = (let n = closest id (\x. \n::nat. even n \ \x\ = real n) {x. \n :: nat. \x\ = real n} (x / y) in x - n * y)" definition frem :: "roundmode \ ('e ,'f) float \ ('e ,'f) float \ ('e ,'f) float" where "frem m a b = (if is_nan a \ is_nan b \ is_infinity a \ is_zero b then some_nan else zerosign (sign a) (round m (rem (valof a) (valof b))))" subsection \Definitions of the arithmetic operations\ definition fintrnd :: "roundmode \ ('e ,'f) float \ ('e ,'f) float" where "fintrnd m a = (if is_nan a then (some_nan) else if is_infinity a then a else zerosign (sign a) (intround m (valof a)))" definition fadd :: "roundmode \ ('e ,'f) float \ ('e ,'f) float \ ('e ,'f) float" where "fadd m a b = (if is_nan a \ is_nan b \ (is_infinity a \ is_infinity b \ sign a \ sign b) then some_nan else if (is_infinity a) then a else if (is_infinity b) then b else zerosign (if is_zero a \ is_zero b \ sign a = sign b then sign a else if m = roundTowardNegative then 1 else 0) (round m (valof a + valof b)))" definition fsub :: "roundmode \ ('e ,'f) float \ ('e ,'f) float \ ('e ,'f) float" where "fsub m a b = (if is_nan a \ is_nan b \ (is_infinity a \ is_infinity b \ sign a = sign b) then some_nan else if is_infinity a then a else if is_infinity b then - b else zerosign (if is_zero a \ is_zero b \ sign a \ sign b then sign a else if m = roundTowardNegative then 1 else 0) (round m (valof a - valof b)))" definition fmul :: "roundmode \ ('e ,'f) float \ ('e ,'f) float \ ('e ,'f) float" where "fmul m a b = (if is_nan a \ is_nan b \ (is_zero a \ is_infinity b) \ (is_infinity a \ is_zero b) then some_nan else if is_infinity a \ is_infinity b then (if sign a = sign b then plus_infinity else minus_infinity) else zerosign (if sign a = sign b then 0 else 1 ) (round m (valof a * valof b)))" definition fdiv :: "roundmode \ ('e ,'f) float \ ('e ,'f) float \ ('e ,'f) float" where "fdiv m a b = (if is_nan a \ is_nan b \ (is_zero a \ is_zero b) \ (is_infinity a \ is_infinity b) then some_nan else if is_infinity a \ is_zero b then (if sign a = sign b then plus_infinity else minus_infinity) else if is_infinity b then (if sign a = sign b then 0 else - 0) else zerosign (if sign a = sign b then 0 else 1) (round m (valof a / valof b)))" definition fsqrt :: "roundmode \ ('e ,'f) float \ ('e ,'f) float" where "fsqrt m a = (if is_nan a then some_nan else if is_zero a \ is_infinity a \ sign a = 0 then a else if sign a = 1 then some_nan else zerosign (sign a) (round m (sqrt (valof a))))" definition fmul_add :: "roundmode \ ('t ,'w) float \ ('t ,'w) float \ ('t ,'w) float \ ('t ,'w) float" where "fmul_add mode x y z = (let signP = if sign x = sign y then 0 else 1; infP = is_infinity x \ is_infinity y in if is_nan x \ is_nan y \ is_nan z then some_nan else if is_infinity x \ is_zero y \ is_zero x \ is_infinity y \ is_infinity z \ infP \ signP \ sign z then some_nan else if is_infinity z \ (sign z = 0) \ infP \ (signP = 0) then plus_infinity else if is_infinity z \ (sign z = 1) \ infP \ (signP = 1) then minus_infinity else let r1 = valof x * valof y; r2 = valof z; r = r1+r2 in if r=0 then ( \ \Exact Zero Case. Same sign rules as for add apply. \ if r1=0 \ r2=0 \ signP=sign z then zerosign signP 0 else if mode = roundTowardNegative then -0 else 0 ) else ( \ \Not exactly zero: Rounding has sign of exact value, even if rounded val is zero\ zerosign (if r<0 then 1 else 0) (round mode r) ) )" subsection \Comparison operations\ datatype ccode = Gt | Lt | Eq | Und definition fcompare :: "('e ,'f) float \ ('e ,'f) float \ ccode" where "fcompare a b = (if is_nan a \ is_nan b then Und else if is_infinity a \ sign a = 1 then (if is_infinity b \ sign b = 1 then Eq else Lt) else if is_infinity a \ sign a = 0 then (if is_infinity b \ sign b = 0 then Eq else Gt) else if is_infinity b \ sign b = 1 then Gt else if is_infinity b \ sign b = 0 then Lt else if valof a < valof b then Lt else if valof a = valof b then Eq else Gt)" definition flt :: "('e ,'f) float \ ('e ,'f) float \ bool" where "flt a b \ fcompare a b = Lt" definition fle :: "('e ,'f) float \ ('e ,'f) float \ bool" where "fle a b \ fcompare a b = Lt \ fcompare a b = Eq" definition fgt :: "('e ,'f) float \ ('e ,'f) float \ bool" where "fgt a b \ fcompare a b = Gt" definition fge :: "('e ,'f) float \ ('e ,'f) float \ bool" where "fge a b \ fcompare a b = Gt \ fcompare a b = Eq" definition feq :: "('e ,'f) float \ ('e ,'f) float \ bool" where "feq a b \ fcompare a b = Eq" section \Specify float to be double precision and round to even\ instantiation float :: (len, len) plus begin definition plus_float :: "('a, 'b) float \ ('a, 'b) float \ ('a, 'b) float" where "a + b = fadd RNE a b" instance .. end instantiation float :: (len, len) minus begin definition minus_float :: "('a, 'b) float \ ('a, 'b) float \ ('a, 'b) float" where "a - b = fsub RNE a b" instance .. end instantiation float :: (len, len) times begin definition times_float :: "('a, 'b) float \ ('a, 'b) float \ ('a, 'b) float" where "a * b = fmul RNE a b" instance .. end instantiation float :: (len, len) one begin lift_definition one_float :: "('a, 'b) float" is "(0, 2^(LENGTH('a) - 1) - 1, 0)" . instance .. end instantiation float :: (len, len) inverse begin definition divide_float :: "('a, 'b) float \ ('a, 'b) float \ ('a, 'b) float" where "a div b = fdiv RNE a b" definition inverse_float :: "('a, 'b) float \ ('a, 'b) float" where "inverse_float a = fdiv RNE 1 a" instance .. end definition float_rem :: "('a, 'b) float \ ('a, 'b) float \ ('a, 'b) float" where "float_rem a b = frem RNE a b" definition float_sqrt :: "('a, 'b) float \ ('a, 'b) float" where "float_sqrt a = fsqrt RNE a" definition ROUNDFLOAT ::"('a, 'b) float \ ('a, 'b) float" where "ROUNDFLOAT a = fintrnd RNE a" instantiation float :: (len, len) ord begin definition less_float :: "('a, 'b) float \ ('a, 'b) float \ bool" where "a < b \ flt a b" definition less_eq_float :: "('a, 'b) float \ ('a, 'b) float \ bool" where "a \ b \ fle a b" instance .. end definition float_eq :: "('a, 'b) float \ ('a, 'b) float \ bool" (infixl "\" 70) where "float_eq a b = feq a b" instantiation float :: (len, len) abs begin definition abs_float :: "('a, 'b) float \ ('a, 'b) float" where "abs_float a = (if sign a = 0 then a else - a)" instance .. end text \The \1 + \\ property.\ definition normalizes :: "_ itself \ real \ bool" where "normalizes float_format x = (1/ (2::real)^(bias float_format - 1) \ \x\ \ \x\ < threshold float_format)" end diff --git a/thys/IEEE_Floating_Point/IEEE_Properties.thy b/thys/IEEE_Floating_Point/IEEE_Properties.thy --- a/thys/IEEE_Floating_Point/IEEE_Properties.thy +++ b/thys/IEEE_Floating_Point/IEEE_Properties.thy @@ -1,1026 +1,1026 @@ (* Author: Lei Yu, University of Cambridge Author: Fabian Hellauer Fabian Immler *) section \Proofs of Properties about Floating Point Arithmetic\ theory IEEE_Properties imports IEEE begin subsection \Theorems derived from definitions\ lemma valof_eq: "valof x = (if exponent x = 0 then (- 1) ^ sign x * (2 / 2 ^ bias TYPE(('a, 'b) float)) * (real (fraction x) / 2 ^ LENGTH('b)) else (- 1) ^ sign x * (2 ^ exponent x / 2 ^ bias TYPE(('a, 'b) float)) * (1 + real (fraction x) / 2 ^ LENGTH('b)))" for x::"('a, 'b) float" unfolding Let_def by transfer (auto simp: bias_def divide_simps unat_eq_0) lemma exponent_le [simp]: \exponent a \ mask LENGTH('a)\ for a :: \('a, _) float\ by transfer (auto simp add: of_nat_mask_eq intro: word_unat_less_le split: prod.split) lemma exponent_not_less [simp]: \\ mask LENGTH('a) < IEEE.exponent a\ for a :: \('a, _) float\ by (simp add: not_less) lemma infinity_simps: "sign (plus_infinity::('e, 'f)float) = 0" "sign (minus_infinity::('e, 'f)float) = 1" "exponent (plus_infinity::('e, 'f)float) = emax TYPE(('e, 'f)float)" "exponent (minus_infinity::('e, 'f)float) = emax TYPE(('e, 'f)float)" "fraction (plus_infinity::('e, 'f)float) = 0" "fraction (minus_infinity::('e, 'f)float) = 0" subgoal by transfer auto subgoal by transfer auto subgoal by transfer (simp add: emax_def mask_eq_exp_minus_1) subgoal by transfer (simp add: emax_def mask_eq_exp_minus_1) subgoal by transfer auto subgoal by transfer auto done lemma zero_simps: "sign (0::('e, 'f)float) = 0" "sign (- 0::('e, 'f)float) = 1" "exponent (0::('e, 'f)float) = 0" "exponent (- 0::('e, 'f)float) = 0" "fraction (0::('e, 'f)float) = 0" "fraction (- 0::('e, 'f)float) = 0" subgoal by transfer auto subgoal by transfer auto subgoal by transfer auto subgoal by transfer auto subgoal by transfer auto subgoal by transfer auto done lemma emax_eq: "emax x = 2 ^ LENGTH('e) - 1" for x::"('e, 'f)float itself" by (simp add: emax_def unsigned_minus_1_eq_mask mask_eq_exp_minus_1) lemma topfloat_simps: "sign (topfloat::('e, 'f)float) = 0" "exponent (topfloat::('e, 'f)float) = emax TYPE(('e, 'f)float) - 1" "fraction (topfloat::('e, 'f)float) = 2 ^ (fracwidth TYPE(('e, 'f)float)) - 1" and bottomfloat_simps: "sign (bottomfloat::('e, 'f)float) = 1" "exponent (bottomfloat::('e, 'f)float) = emax TYPE(('e, 'f)float) - 1" "fraction (bottomfloat::('e, 'f)float) = 2 ^ (fracwidth TYPE(('e, 'f)float)) - 1" subgoal by transfer simp subgoal by transfer (simp add: emax_eq take_bit_minus_small_eq nat_diff_distrib nat_power_eq) subgoal by transfer (simp add: unsigned_minus_1_eq_mask mask_eq_exp_minus_1) subgoal by transfer simp subgoal by transfer (simp add: emax_eq take_bit_minus_small_eq nat_diff_distrib nat_power_eq) subgoal by transfer (simp add: unsigned_minus_1_eq_mask mask_eq_exp_minus_1) done lemmas float_defs = is_finite_def is_infinity_def is_zero_def is_nan_def is_normal_def is_denormal_def valof_eq less_eq_float_def less_float_def flt_def fgt_def fle_def fge_def feq_def fcompare_def infinity_simps zero_simps topfloat_simps bottomfloat_simps float_eq_def lemma float_cases: "is_nan a \ is_infinity a \ is_normal a \ is_denormal a \ is_zero a" by (auto simp add: float_defs not_less le_less emax_def unsigned_minus_1_eq_mask) lemma float_cases_finite: "is_nan a \ is_infinity a \ is_finite a" by (simp add: float_cases is_finite_def) lemma float_zero1[simp]: "is_zero 0" unfolding float_defs by transfer auto lemma float_zero2[simp]: "is_zero (- x) \ is_zero x" unfolding float_defs by transfer auto lemma emax_pos[simp]: "0 < emax x" "emax x \ 0" by (auto simp: emax_def) text \The types of floating-point numbers are mutually distinct.\ lemma float_distinct: "\ (is_nan a \ is_infinity a)" "\ (is_nan a \ is_normal a)" "\ (is_nan a \ is_denormal a)" "\ (is_nan a \ is_zero a)" "\ (is_infinity a \ is_normal a)" "\ (is_infinity a \ is_denormal a)" "\ (is_infinity a \ is_zero a)" "\ (is_normal a \ is_denormal a)" "\ (is_denormal a \ is_zero a)" by (auto simp: float_defs) lemma denormal_imp_not_zero: "is_denormal f \ \is_zero f" by (simp add: is_denormal_def is_zero_def) lemma normal_imp_not_zero: "is_normal f \ \is_zero f" by (simp add: is_normal_def is_zero_def) lemma normal_imp_not_denormal: "is_normal f \ \is_denormal f" by (simp add: is_normal_def is_denormal_def) lemma denormal_zero[simp]: "\is_denormal 0" "\is_denormal minus_zero" using denormal_imp_not_zero float_zero1 float_zero2 by blast+ lemma normal_zero[simp]: "\is_normal 0" "\is_normal minus_zero" using normal_imp_not_zero float_zero1 float_zero2 by blast+ lemma float_distinct_finite: "\ (is_nan a \ is_finite a)" "\(is_infinity a \ is_finite a)" by (auto simp: float_defs) lemma finite_infinity: "is_finite a \ \ is_infinity a" by (auto simp: float_defs) lemma finite_nan: "is_finite a \ \ is_nan a" by (auto simp: float_defs) text \For every real number, the floating-point numbers closest to it always exist.\ lemma is_closest_exists: fixes v :: "('e, 'f)float \ real" and s :: "('e, 'f)float set" assumes finite: "finite s" and non_empty: "s \ {}" shows "\a. is_closest v s x a" using finite non_empty proof (induct s rule: finite_induct) case empty then show ?case by simp next case (insert z s) show ?case proof (cases "s = {}") case True then have "is_closest v (insert z s) x z" by (auto simp: is_closest_def) then show ?thesis by metis next case False then obtain a where a: "is_closest v s x a" using insert by metis then show ?thesis proof (cases "\v a - x\" "\v z - x\" rule: le_cases) case le then show ?thesis by (metis insert_iff a is_closest_def) next case ge have "\b. b \ s \ \v a - x\ \ \v b - x\" by (metis a is_closest_def) then have "\b. b \ insert z s \ \v z - x\ \ \v b - x\" by (metis eq_iff ge insert_iff order.trans) then show ?thesis using is_closest_def a by (metis insertI1) qed qed qed lemma closest_is_everything: fixes v :: "('e, 'f)float \ real" and s :: "('e, 'f)float set" assumes finite: "finite s" and non_empty: "s \ {}" shows "is_closest v s x (closest v p s x) \ ((\b. is_closest v s x b \ p b) \ p (closest v p s x))" unfolding closest_def by (rule someI_ex) (metis assms is_closest_exists [of s v x]) lemma closest_in_set: fixes v :: "('e, 'f)float \ real" assumes "finite s" and "s \ {}" shows "closest v p s x \ s" by (metis assms closest_is_everything is_closest_def) lemma closest_is_closest_finite: fixes v :: "('e, 'f)float \ real" assumes "finite s" and "s \ {}" shows "is_closest v s x (closest v p s x)" by (metis closest_is_everything assms) instance float::(len, len) finite proof qed (transfer, simp) lemma is_finite_nonempty: "{a. is_finite a} \ {}" proof - have "0 \ {a. is_finite a}" unfolding float_defs by transfer auto then show ?thesis by (metis empty_iff) qed lemma closest_is_closest: fixes v :: "('e, 'f)float \ real" assumes "s \ {}" shows "is_closest v s x (closest v p s x)" by (rule closest_is_closest_finite) (auto simp: assms) subsection \Properties about ordering and bounding\ text \Lifting of non-exceptional comparisons.\ lemma float_lt [simp]: assumes "is_finite a" "is_finite b" shows "a < b \ valof a < valof b" proof assume "valof a < valof b" moreover have "\ is_nan a" and "\ is_nan b" and "\ is_infinity a" and "\ is_infinity b" using assms by (auto simp: finite_nan finite_infinity) ultimately have "fcompare a b = Lt" by (auto simp add: is_infinity_def is_nan_def valof_def fcompare_def) then show "a < b" by (auto simp: float_defs) next assume "a < b" then have lt: "fcompare a b = Lt" by (simp add: float_defs) have "\ is_nan a" and "\ is_nan b" and "\ is_infinity a" and "\ is_infinity b" using assms by (auto simp: finite_nan finite_infinity) then show "valof a < valof b" using lt assms by (simp add: fcompare_def is_nan_def is_infinity_def valof_def split: if_split_asm) qed lemma float_eq [simp]: assumes "is_finite a" "is_finite b" shows "a \ b \ valof a = valof b" proof assume *: "valof a = valof b" have "\ is_nan a" and "\ is_nan b" and "\ is_infinity a" and "\ is_infinity b" using assms float_distinct_finite by auto with * have "fcompare a b = Eq" by (auto simp add: is_infinity_def is_nan_def valof_def fcompare_def) then show "a \ b" by (auto simp: float_defs) next assume "a \ b" then have eq: "fcompare a b = Eq" by (simp add: float_defs) have "\ is_nan a" and "\ is_nan b" and "\ is_infinity a" and "\ is_infinity b" using assms float_distinct_finite by auto then show "valof a = valof b" using eq assms by (simp add: fcompare_def is_nan_def is_infinity_def valof_def split: if_split_asm) qed lemma float_le [simp]: assumes "is_finite a" "is_finite b" shows "a \ b \ valof a \ valof b" proof - have "a \ b \ a < b \ a \ b" by (auto simp add: float_defs) then show ?thesis by (auto simp add: assms) qed text \Reflexivity of equality for non-NaNs.\ lemma float_eq_refl [simp]: "a \ a \ \ is_nan a" by (auto simp: float_defs) text \Properties about Ordering.\ lemma float_lt_trans: "is_finite a \ is_finite b \ is_finite c \ a < b \ b < c \ a < c" by (auto simp: le_trans) lemma float_le_less_trans: "is_finite a \ is_finite b \ is_finite c \ a \ b \ b < c \ a < c" by (auto simp: le_trans) lemma float_le_trans: "is_finite a \ is_finite b \ is_finite c \ a \ b \ b \ c \ a \ c" by (auto simp: le_trans) lemma float_le_neg: "is_finite a \ is_finite b \ \ a < b \ b \ a" by auto text \Properties about bounding.\ lemma float_le_infinity [simp]: "\ is_nan a \ a \ plus_infinity" unfolding float_defs by auto lemma zero_le_topfloat[simp]: "0 \ topfloat" "- 0 \ topfloat" by (auto simp: float_defs field_simps power_gt1_lemma of_nat_diff mask_eq_exp_minus_1) lemma LENGTH_contr: "Suc 0 < LENGTH('e) \ 2 ^ LENGTH('e::len) \ Suc (Suc 0) \ False" by (metis le_antisym len_gt_0 n_less_equal_power_2 not_less_eq numeral_2_eq_2 one_le_numeral self_le_power) lemma valof_topfloat: "valof (topfloat::('e, 'f)float) = largest TYPE(('e, 'f)float)" if "LENGTH('e) > 1" using that LENGTH_contr by (auto simp add: emax_eq largest_def divide_simps float_defs of_nat_diff mask_eq_exp_minus_1) lemma float_frac_le: "fraction a \ 2^LENGTH('f) - 1" for a::"('e, 'f)float" unfolding float_defs using less_Suc_eq_le by transfer fastforce lemma float_exp_le: "is_finite a \ exponent a \ emax TYPE(('e, 'f)float) - 1" for a::"('e, 'f)float" unfolding float_defs by auto lemma float_sign_le: "(-1::real)^(sign a) = 1 \ (-1::real)^(sign a) = -1" by (metis neg_one_even_power neg_one_odd_power) lemma exp_less: "a \ b \ (2::real)^a \ 2^b" for a b :: nat by auto lemma div_less: "a \ b \ c > 0 \ a/c \ b/c" for a b c :: "'a::linordered_field" by (metis divide_le_cancel less_asym) lemma finite_topfloat: "is_finite topfloat" unfolding float_defs by auto lemmas float_leI = float_le[THEN iffD2] lemma factor_minus: "x * a - x = x * (a - 1)" for x a::"'a::comm_semiring_1_cancel" by (simp add: algebra_simps) lemma real_le_power_numeral_diff: "real a \ numeral b ^ n - 1 \ a \ numeral b ^ n - 1" by (metis (mono_tags, lifting) of_nat_1 of_nat_diff of_nat_le_iff of_nat_numeral one_le_numeral one_le_power semiring_1_class.of_nat_power) definition denormal_exponent::"('e, 'f)float itself \ int" where "denormal_exponent x = 1 - (int (LENGTH('f)) + int (bias TYPE(('e, 'f)float)))" definition normal_exponent::"('e, 'f)float \ int" where "normal_exponent x = int (exponent x) - int (bias TYPE(('e, 'f)float)) - int (LENGTH('f))" definition denormal_mantissa::"('e, 'f)float \ int" where "denormal_mantissa x = (-1::int)^sign x * int (fraction x)" definition normal_mantissa::"('e, 'f)float \ int" where "normal_mantissa x = (-1::int)^sign x * (2^LENGTH('f) + int (fraction x))" lemma unat_one_word_le: "unat a \ Suc 0" for a::"1 word" using unat_lt2p[of a] by auto lemma one_word_le: "a \ 1" for a::"1 word" by (auto simp: word_le_nat_alt unat_one_word_le) lemma sign_cases[case_names pos neg]: obtains "sign x = 0" | "sign x = 1" proof cases assume "sign x = 0" then show ?thesis .. next assume "sign x \ 0" have "sign x \ 1" by transfer (auto simp: unat_one_word_le) then have "sign x = 1" using \sign x \ 0\ by auto then show ?thesis .. qed lemma is_infinity_cases: assumes "is_infinity x" obtains "x = plus_infinity" | "x = minus_infinity" proof (cases rule: sign_cases[of x]) assume "sign x = 0" then have "x = plus_infinity" using assms apply (unfold float_defs) apply transfer apply (auto simp add: unat_eq_of_nat emax_def of_nat_mask_eq) done then show ?thesis .. next assume "sign x = 1" then have "x = minus_infinity" using assms apply (unfold float_defs) apply transfer apply (auto simp add: unat_eq_of_nat emax_def of_nat_mask_eq) done then show ?thesis .. qed lemma is_zero_cases: assumes "is_zero x" obtains "x = 0" | "x = - 0" proof (cases rule: sign_cases[of x]) assume "sign x = 0" then have "x = 0" using assms unfolding float_defs by transfer (auto simp: emax_def unat_eq_0) then show ?thesis .. next assume "sign x = 1" then have "x = minus_zero" using assms unfolding float_defs by transfer (auto simp: emax_def unat_eq_of_nat) then show ?thesis .. qed lemma minus_minus_float[simp]: "- (-f) = f" for f::"('e, 'f)float" by transfer auto lemma sign_minus_float: "sign (-f) = (1 - sign f)" for f::"('e, 'f)float" by transfer (auto simp: unat_eq_1 one_word_le unat_sub) lemma exponent_uminus[simp]: "exponent (- f) = exponent f" by transfer auto lemma fraction_uminus[simp]: "fraction (- f) = fraction f" by transfer auto lemma is_normal_minus_float[simp]: "is_normal (-f) = is_normal f" for f::"('e, 'f)float" by (auto simp: is_normal_def) lemma is_denormal_minus_float[simp]: "is_denormal (-f) = is_denormal f" for f::"('e, 'f)float" by (auto simp: is_denormal_def) lemma bitlen_normal_mantissa: "bitlen (abs (normal_mantissa x)) = Suc LENGTH('f)" for x::"('e, 'f)float" proof - have "fraction x < 2 ^ LENGTH('f)" using float_frac_le[of x] by (metis One_nat_def Suc_pred le_imp_less_Suc pos2 zero_less_power) moreover have "- int (fraction x) \ 2 ^ LENGTH('f)" using negative_zle_0 order_trans zero_le_numeral zero_le_power by blast ultimately show ?thesis by (cases x rule: sign_cases) (auto simp: bitlen_le_iff_power bitlen_ge_iff_power nat_add_distrib normal_mantissa_def intro!: antisym) qed lemma less_int_natI: "x < y" if "0 \ x" "nat x < nat y" using that by arith lemma normal_exponent_bounds_int: "2 - 2 ^ (LENGTH('e) - 1) - int LENGTH('f) \ normal_exponent x" "normal_exponent x \ 2 ^ (LENGTH('e) - 1) - int LENGTH('f) - 1" if "is_normal x" for x::"('e, 'f)float" using that apply (auto simp add: normal_exponent_def is_normal_def emax_eq bias_def diff_le_eq diff_less_eq mask_eq_exp_minus_1 of_nat_diff simp flip: zless_nat_eq_int_zless power_Suc) apply (simp flip: power_Suc mask_eq_exp_minus_1 add: nat_mask_eq) apply (simp add: mask_eq_exp_minus_1) done lemmas of_int_leI = of_int_le_iff[THEN iffD2] lemma normal_exponent_bounds_real: "2 - 2 ^ (LENGTH('e) - 1) - real LENGTH('f) \ normal_exponent x" "normal_exponent x \ 2 ^ (LENGTH('e) - 1) - real LENGTH('f) - 1" if "is_normal x" for x::"('e, 'f)float" subgoal by (rule order_trans[OF _ of_int_leI[OF normal_exponent_bounds_int(1)[OF that]]]) auto subgoal by (rule order_trans[OF of_int_leI[OF normal_exponent_bounds_int(2)[OF that]]]) auto done lemma float_eqI: "x = y" if "sign x = sign y" "fraction x = fraction y" "exponent x = exponent y" using that by transfer (auto simp add: word_unat_eq_iff) lemma float_induct[induct type:float, case_names normal denormal neg zero infinity nan]: fixes a::"('e, 'f)float" assumes normal: "\x. is_normal x \ valof x = normal_mantissa x * 2 powr normal_exponent x \ P x" assumes denormal: "\x. is_denormal x \ valof x = denormal_mantissa x * 2 powr denormal_exponent TYPE(('e, 'f)float) \ P x" assumes zero: "P 0" "P minus_zero" assumes infty: "P plus_infinity" "P minus_infinity" assumes nan: "\x. is_nan x \ P x" shows "P a" proof - from float_cases[of a] consider "is_nan a" | "is_infinity a" | "is_normal a" | "is_denormal a" | "is_zero a" by blast then show ?thesis proof cases case 1 then show ?thesis by (rule nan) next case 2 then consider "a = plus_infinity" | "a = minus_infinity" by (rule is_infinity_cases) then show ?thesis by cases (auto intro: infty) next case hyps: 3 from hyps have "valof a = normal_mantissa a * 2 powr normal_exponent a" by (cases a rule: sign_cases) (auto simp: valof_eq normal_mantissa_def normal_exponent_def is_normal_def powr_realpow[symmetric] powr_diff powr_add field_simps) from hyps this show ?thesis by (rule normal) next case hyps: 4 from hyps have "valof a = denormal_mantissa a * 2 powr denormal_exponent TYPE(('e, 'f)float)" by (cases a rule: sign_cases) (auto simp: valof_eq denormal_mantissa_def denormal_exponent_def is_denormal_def powr_realpow[symmetric] powr_diff powr_add field_simps) from hyps this show ?thesis by (rule denormal) next case 5 then consider "a = 0" | "a = minus_zero" by (rule is_zero_cases) then show ?thesis by cases (auto intro: zero) qed qed lemma infinite_infinity[simp]: "\ is_finite plus_infinity" "\ is_finite minus_infinity" by (auto simp: is_finite_def is_normal_def infinity_simps is_denormal_def is_zero_def) lemma nan_not_finite[simp]: "is_nan x \ \ is_finite x" using float_distinct_finite(1) by blast lemma valof_nonneg: "valof x \ 0" if "sign x = 0" for x::"('e, 'f)float" by (auto simp: valof_eq that) lemma valof_nonpos: "valof x \ 0" if "sign x = 1" for x::"('e, 'f)float" using that by (auto simp: valof_eq is_finite_def) lemma real_le_intI: "x \ y" if "floor x \ floor y" "x \ \" for x y::real using that(2,1) by (induction rule: Ints_induct) (auto elim!: Ints_induct simp: le_floor_iff) lemma real_of_int_le_2_powr_bitlenI: "real_of_int x \ 2 powr n - 1" if "bitlen (abs x) \ m" "m \ n" proof - have "real_of_int x \ abs (real_of_int x)" by simp also have "\ < 2 powr (bitlen (abs x))" by (rule abs_real_le_2_powr_bitlen) finally have "real_of_int x \ 2 powr (bitlen (abs x)) - 1" by (auto simp: powr_real_of_int bitlen_nonneg intro!: real_le_intI) also have "\ \ 2 powr m - 1" by (simp add: that) also have "\ \ 2 powr n - 1" by (simp add: that) finally show ?thesis . qed lemma largest_eq: "largest TYPE(('e, 'f)float) = (2 ^ (LENGTH('f) + 1) - 1) * 2 powr real_of_int (2 ^ (LENGTH('e) - 1) - int LENGTH('f) - 1)" proof - have "2 ^ LENGTH('e) - 1 - 1 = (2::nat) ^ LENGTH('e) - 2" by arith then have "largest TYPE(('e, 'f)float) = (2 ^ (LENGTH('f) + 1) - 1) * 2 powr (real (2 ^ LENGTH('e) - 2) + 1 - real (2 ^ (LENGTH('e) - 1)) - LENGTH('f))" by (auto simp add: largest_def emax_eq bias_def powr_minus field_simps powr_diff powr_add of_nat_diff mask_eq_exp_minus_1 simp flip: powr_realpow) also have "2 ^ LENGTH('e) \ (2::nat)" by (simp add: self_le_power) then have "(real (2 ^ LENGTH('e) - 2) + 1 - real (2 ^ (LENGTH('e) - 1)) - LENGTH('f)) = (real (2 ^ LENGTH('e)) - 2 ^ (LENGTH('e) - 1) - LENGTH('f)) - 1" by (auto simp add: of_nat_diff) also have "real (2 ^ LENGTH('e)) = 2 ^ LENGTH('e)" by auto also have "(2 ^ LENGTH('e) - 2 ^ (LENGTH('e) - 1) - real LENGTH('f) - 1) = real_of_int ((2 ^ (LENGTH('e) - 1) - int (LENGTH('f)) - 1))" by (simp, subst power_Suc[symmetric], simp) finally show ?thesis by simp qed lemma bitlen_denormal_mantissa: "bitlen (abs (denormal_mantissa x)) \ LENGTH('f)" for x::"('e, 'f)float" proof - have "fraction x < 2 ^ LENGTH('f)" using float_frac_le[of x] by (metis One_nat_def Suc_pred le_imp_less_Suc pos2 zero_less_power) moreover have "- int (fraction x) \ 2 ^ LENGTH('f)" using negative_zle_0 order_trans zero_le_numeral zero_le_power by blast ultimately show ?thesis by (cases x rule: sign_cases) (auto simp: bitlen_le_iff_power denormal_mantissa_def intro!: antisym) qed lemma float_le_topfloat: fixes a::"('e, 'f)float" assumes "is_finite a" "LENGTH('e) > 1" shows "a \ topfloat" using assms(1) proof (induction a rule: float_induct) case (normal x) note normal(2) also have "real_of_int (normal_mantissa x) * 2 powr real_of_int (normal_exponent x) \ (2 powr (LENGTH('f) + 1) - 1) * 2 powr (2 ^ (LENGTH('e) - 1) - int LENGTH('f) - 1)" using normal_exponent_bounds_real(2)[OF \is_normal x\] by (auto intro!: mult_mono real_of_int_le_2_powr_bitlenI simp: bitlen_normal_mantissa powr_realpow[symmetric] ge_one_powr_ge_zero) also have "\ = largest TYPE(('e, 'f) IEEE.float)" unfolding largest_eq by (auto simp: powr_realpow powr_add) also have "\ = valof (topfloat::('e, 'f) float)" using assms by (simp add: valof_topfloat) finally show ?case by (intro float_leI normal finite_topfloat) next case (denormal x) note denormal(2) also have "3 \ 2 powr (1 + real (LENGTH('e) - Suc 0))" proof - have "3 \ 2 powr (2::real)" by simp also have "\ \ 2 powr (1 + real (LENGTH('e) - Suc 0))" using assms by (subst powr_le_cancel_iff) auto finally show ?thesis . qed then have "real_of_int (denormal_mantissa x) * 2 powr real_of_int (denormal_exponent TYPE(('e, 'f)float)) \ (2 powr (LENGTH('f) + 1) - 1) * 2 powr (2 ^ (LENGTH('e) - 1) - int LENGTH('f) - 1)" using bitlen_denormal_mantissa[of x] by (auto intro!: mult_mono real_of_int_le_2_powr_bitlenI simp: bitlen_normal_mantissa powr_realpow[symmetric] ge_one_powr_ge_zero mask_eq_exp_minus_1 denormal_exponent_def bias_def powr_mult_base of_nat_diff) also have "\ \ largest TYPE(('e, 'f) IEEE.float)" unfolding largest_eq by (rule mult_mono) (auto simp: powr_realpow powr_add power_Suc[symmetric] simp del: power_Suc) also have "\ = valof (topfloat::('e, 'f) float)" using assms by (simp add: valof_topfloat) finally show ?case by (intro float_leI denormal finite_topfloat) qed auto lemma float_val_le_largest: "valof a \ largest TYPE(('e, 'f)float)" if "is_finite a" "LENGTH('e) > 1" for a::"('e, 'f)float" by (metis that finite_topfloat float_le float_le_topfloat valof_topfloat) lemma float_val_lt_threshold: "valof a < threshold TYPE(('e, 'f)float)" if "is_finite a" "LENGTH('e) > 1" for a::"('e, 'f)float" proof - have "valof a \ largest TYPE(('e, 'f)float)" by (rule float_val_le_largest [OF that]) also have "\ < threshold TYPE(('e, 'f)float)" by (auto simp: largest_def threshold_def divide_simps) finally show ?thesis . qed subsection \Algebraic properties about basic arithmetic\ text \Commutativity of addition.\ lemma assumes "is_finite a" "is_finite b" shows float_plus_comm_eq: "a + b = b + a" and float_plus_comm: "is_finite (a + b) \ (a + b) \ (b + a)" proof - have "\ is_nan a" and "\ is_nan b" and "\ is_infinity a" and "\ is_infinity b" using assms by (auto simp: finite_nan finite_infinity) then show "a + b = b + a" by (simp add: float_defs fadd_def plus_float_def add.commute) then show "is_finite (a + b) \ (a + b) \ (b + a)" by (metis float_eq) qed text \The floating-point number a falls into the same category as the negation of \a\.\ lemma is_zero_uminus[simp]: "is_zero (- a) \ is_zero a" by (simp add: is_zero_def) lemma is_infinity_uminus [simp]: "is_infinity (- a) = is_infinity a" by (simp add: is_infinity_def) lemma is_finite_uminus[simp]: "is_finite (- a) \ is_finite a" by (simp add: is_finite_def) lemma is_nan_uminus[simp]: "is_nan (- a) \ is_nan a" by (simp add: is_nan_def) text \The sign of a and the sign of a's negation is different.\ lemma float_neg_sign: "(sign a) \ (sign (- a))" by (cases a rule: sign_cases) (auto simp: sign_minus_float) lemma float_neg_sign1: "sign a = sign (- b) \ sign a \ sign b" by (metis float_neg_sign sign_cases) lemma valof_uminus: assumes "is_finite a" shows "valof (- a) = - valof a" (is "?L = ?R") by (cases a rule: sign_cases) (auto simp: valof_eq sign_minus_float) text \Showing \a + (- b) = a - b\.\ -lemma float_neg_add: +lemma float_neg_add: (*FIXME*) "is_finite a \ is_finite b \ is_finite (a - b) \ valof a + valof (- b) = valof a - valof b" by (simp add: valof_uminus) lemma float_plus_minus: assumes "is_finite a" "is_finite b" "is_finite (a - b)" shows "(a + - b) \ (a - b)" proof - have nab: "\ is_nan a" "\ is_nan (- b)" "\ is_infinity a" "\ is_infinity (- b)" using assms by (auto simp: finite_nan finite_infinity) have "a - b = (zerosign (if is_zero a \ is_zero b \ sign a \ sign b then (sign a) else 0) (round RNE (valof a - valof b)))" using nab by (auto simp: minus_float_def fsub_def) also have "\ = (zerosign (if is_zero a \ is_zero (- b) \ sign a = sign (- b) then sign a else 0) (round RNE (valof a + valof (- b))))" using assms by (simp add: float_neg_sign1 float_neg_add) also have "\ = a + - b" using nab by (auto simp: float_defs fadd_def plus_float_def) finally show ?thesis using assms by (metis float_eq) qed lemma finite_bottomfloat: "is_finite bottomfloat" by (simp add: finite_topfloat) lemma bottomfloat_eq_m_largest: "valof (bottomfloat::('e, 'f)float) = - largest TYPE(('e, 'f)float)" if "LENGTH('e) > 1" using that by (auto simp: valof_topfloat valof_uminus finite_topfloat) lemma float_val_ge_bottomfloat: "valof a \ valof (bottomfloat::('e, 'f)float)" if "LENGTH('e) > 1" "is_finite a" for a::"('e,'f)float" proof - have "- a \ topfloat" using that by (auto intro: float_le_topfloat) then show ?thesis using that by (auto simp: valof_uminus finite_topfloat) qed lemma float_ge_bottomfloat: "is_finite a \ a \ bottomfloat" if "LENGTH('e) > 1" "is_finite a" for a::"('e,'f)float" by (metis finite_bottomfloat float_le float_val_ge_bottomfloat that) lemma float_val_ge_largest: fixes a::"('e,'f)float" assumes "LENGTH('e) > 1" "is_finite a" shows "valof a \ - largest TYPE(('e,'f)float)" proof - have "- largest TYPE(('e,'f)float) = valof (bottomfloat::('e,'f)float)" using assms by (simp add: bottomfloat_eq_m_largest) also have "\ \ valof a" using assms by (simp add: float_val_ge_bottomfloat) finally show ?thesis . qed lemma float_val_gt_threshold: fixes a::"('e,'f)float" assumes "LENGTH('e) > 1" "is_finite a" shows "valof a > - threshold TYPE(('e,'f)float)" proof - have largest: "valof a \ -largest TYPE(('e,'f)float)" using assms by (metis float_val_ge_largest) then have "-largest TYPE(('e,'f)float) > - threshold TYPE(('e,'f)float)" by (auto simp: bias_def threshold_def largest_def divide_simps) then show ?thesis by (metis largest less_le_trans) qed text \Showing \abs (- a) = abs a\.\ lemma float_abs [simp]: "\ is_nan a \ abs (- a) = abs a" by (metis IEEE.abs_float_def float_neg_sign1 minus_minus_float zero_simps(1)) lemma neg_zerosign: "- (zerosign s a) = zerosign (1 - s) (- a)" by (auto simp: zerosign_def) subsection \Properties about Rounding Errors\ definition error :: "('e, 'f)float itself \ real \ real" where "error _ x = valof (round RNE x::('e, 'f)float) - x" lemma bound_at_worst_lemma: fixes a::"('e, 'f)float" assumes threshold: "\x\ < threshold TYPE(('e, 'f)float)" assumes finite: "is_finite a" shows "\valof (round RNE x::('e, 'f)float) - x\ \ \valof a - x\" proof - have *: "(round RNE x::('e,'f)float) = closest valof (\a. even (fraction a)) {a. is_finite a} x" using threshold finite by auto have "is_closest (valof) {a. is_finite a} x (round RNE x::('e,'f)float)" using is_finite_nonempty unfolding * by (intro closest_is_closest) auto then show ?thesis using finite is_closest_def by (metis mem_Collect_eq) qed lemma error_at_worst_lemma: fixes a::"('e, 'f)float" assumes threshold: "\x\ < threshold TYPE(('e, 'f)float)" and "is_finite a" shows "\error TYPE(('e, 'f)float) x\ \ \valof a - x\ " unfolding error_def by (rule bound_at_worst_lemma; fact) lemma error_is_zero [simp]: fixes a::"('e, 'f)float" assumes "is_finite a" "1 < LENGTH('e)" shows "error TYPE(('e, 'f)float) (valof a) = 0" proof - have "\valof a\ < threshold TYPE(('e, 'f)float)" by (metis abs_less_iff minus_less_iff float_val_gt_threshold float_val_lt_threshold assms) then show ?thesis by (metis abs_le_zero_iff abs_zero diff_self error_at_worst_lemma assms(1)) qed lemma is_finite_zerosign[simp]: "is_finite (zerosign s a) \ is_finite a" by (auto simp: zerosign_def is_finite_def) lemma is_finite_closest: "is_finite (closest (v::_\real) p {a. is_finite a} x)" using closest_is_closest[OF is_finite_nonempty, of v x p] by (auto simp: is_closest_def) lemma defloat_float_zerosign_round_finite: assumes threshold: "\x\ < threshold TYPE(('e, 'f)float)" shows "is_finite (zerosign s (round RNE x::('e, 'f)float))" proof - have "(round RNE x::('e, 'f)float) = (closest valof (\a. even (fraction a)) {a. is_finite a} x)" using threshold by (metis (full_types) abs_less_iff leD le_minus_iff round.simps(1)) then have "is_finite (round RNE x::('e, 'f)float)" by (metis is_finite_closest) then show ?thesis using is_finite_zerosign by auto qed lemma valof_zero[simp]: "valof 0 = 0" "valof minus_zero = 0" by (auto simp add: zerosign_def valof_eq zero_simps) lemma signzero_zero: "is_zero a \ valof (zerosign s a) = 0" by (auto simp add: zerosign_def) lemma val_zero: "is_zero a \ valof a = 0" by (cases a rule: is_zero_cases) auto lemma float_add: fixes a b::"('e, 'f)float" assumes "is_finite a" and "is_finite b" and threshold: "\valof a + valof b\ < threshold TYPE(('e, 'f)float)" shows finite_float_add: "is_finite (a + b)" and error_float_add: "valof (a + b) = valof a + valof b + error TYPE(('e, 'f)float) (valof a + valof b)" proof - have "\ is_nan a" and "\ is_nan b" and "\ is_infinity a" and "\ is_infinity b" using assms float_distinct_finite by auto then have ab: "(a + b) = (zerosign (if is_zero a \ is_zero b \ sign a = sign b then (sign a) else 0) (round RNE (valof a + valof b)))" using assms by (auto simp add: float_defs fadd_def plus_float_def) then show "is_finite ((a + b))" by (metis threshold defloat_float_zerosign_round_finite) have val_ab: "valof (a + b) = valof (zerosign (if is_zero a \ is_zero b \ sign a = sign b then (sign a) else 0) (round RNE (valof a + valof b)::('e, 'f)float))" by (auto simp: ab is_infinity_def is_nan_def valof_def) show "valof (a + b) = valof a + valof b + error TYPE(('e, 'f)float) (valof a + valof b)" proof (cases "is_zero (round RNE (valof a + valof b)::('e, 'f)float)") case True have "valof a + valof b + error TYPE(('e, 'f)float) (valof a + valof b) = valof (round RNE (valof a + valof b)::('e, 'f)float)" unfolding error_def by simp then show ?thesis by (metis True signzero_zero val_zero val_ab) next case False then show ?thesis by (metis ab add.commute eq_diff_eq' error_def zerosign_def) qed qed lemma float_sub: fixes a b::"('e, 'f)float" assumes "is_finite a" and "is_finite b" and threshold: "\valof a - valof b\ < threshold TYPE(('e, 'f)float)" shows finite_float_sub: "is_finite (a - b)" and error_float_sub: "valof (a - b) = valof a - valof b + error TYPE(('e, 'f)float) (valof a - valof b)" proof - have "\ is_nan a" and "\ is_nan b" and "\ is_infinity a" and "\ is_infinity b" using assms by (auto simp: finite_nan finite_infinity) then have ab: "a - b = (zerosign (if is_zero a \ is_zero b \ sign a \ sign b then sign a else 0) (round RNE (valof a - valof b)))" using assms by (auto simp add: float_defs fsub_def minus_float_def) then show "is_finite (a - b)" by (metis threshold defloat_float_zerosign_round_finite) have val_ab: "valof (a - b) = valof (zerosign (if is_zero a \ is_zero b \ sign a \ sign b then sign a else 0) (round RNE (valof a - valof b)::('e, 'f)float))" by (auto simp: ab is_infinity_def is_nan_def valof_def) show "valof (a - b) = valof a - valof b + error TYPE(('e, 'f)float) (valof a - valof b)" proof (cases "is_zero (round RNE (valof a - valof b)::('e, 'f)float)") case True have "valof a - valof b + error TYPE(('e, 'f)float) (valof a - valof b) = valof (round RNE (valof a - valof b)::('e, 'f)float)" unfolding error_def by simp then show ?thesis by (metis True signzero_zero val_zero val_ab) next case False then show ?thesis by (metis ab add.commute eq_diff_eq' error_def zerosign_def) qed qed lemma float_mul: fixes a b::"('e, 'f)float" assumes "is_finite a" and "is_finite b" and threshold: "\valof a * valof b\ < threshold TYPE(('e, 'f)float)" shows finite_float_mul: "is_finite (a * b)" and error_float_mul: "valof (a * b) = valof a * valof b + error TYPE(('e, 'f)float) (valof a * valof b)" proof - have non: "\ is_nan a" "\ is_nan b" "\ is_infinity a" "\ is_infinity b" using assms float_distinct_finite by auto then have ab: "a * b = (zerosign (of_bool (sign a \ sign b)) (round RNE (valof a * valof b)::('e, 'f)float))" using assms by (auto simp: float_defs fmul_def times_float_def) then show "is_finite (a * b)" by (metis threshold defloat_float_zerosign_round_finite) have val_ab: "valof (a * b) = valof (zerosign (of_bool (sign a \ sign b)) (round RNE (valof a * valof b)::('e, 'f)float))" by (auto simp: ab float_defs of_bool_def) show "valof (a * b) = valof a * valof b + error TYPE(('e, 'f)float) (valof a * valof b)" proof (cases "is_zero (round RNE (valof a * valof b)::('e, 'f)float)") case True have "valof a * valof b + error TYPE(('e, 'f)float) (valof a * valof b) = valof (round RNE (valof a * valof b)::('e, 'f)float)" unfolding error_def by simp then show ?thesis by (metis True signzero_zero val_zero val_ab) next case False then show ?thesis by (metis ab add.commute eq_diff_eq' error_def zerosign_def) qed qed lemma float_div: fixes a b::"('e, 'f)float" assumes "is_finite a" and "is_finite b" and not_zero: "\ is_zero b" and threshold: "\valof a / valof b\ < threshold TYPE(('e, 'f)float)" shows finite_float_div: "is_finite (a / b)" and error_float_div: "valof (a / b) = valof a / valof b + error TYPE(('e, 'f)float) (valof a / valof b)" proof - have ab: "a / b = (zerosign (of_bool (sign a \ sign b)) (round RNE (valof a / valof b)))" using assms by (simp add: divide_float_def fdiv_def finite_infinity finite_nan not_zero float_defs [symmetric]) then show "is_finite (a / b)" by (metis threshold defloat_float_zerosign_round_finite) have val_ab: "valof (a / b) = valof (zerosign (of_bool (sign a \ sign b)) (round RNE (valof a / valof b))::('e, 'f)float)" by (auto simp: ab float_defs of_bool_def) show "valof (a / b) = valof a / valof b + error TYPE(('e, 'f)float) (valof a / valof b)" proof (cases "is_zero (round RNE (valof a / valof b)::('e, 'f)float)") case True have "valof a / valof b + error TYPE(('e, 'f)float) (valof a / valof b) = valof (round RNE (valof a / valof b)::('e, 'f)float)" unfolding error_def by simp then show ?thesis by (metis True signzero_zero val_zero val_ab) next case False then show ?thesis by (metis ab add.commute eq_diff_eq' error_def zerosign_def) qed qed lemma valof_one[simp]: "valof (1 :: ('e, 'f) float) = of_bool (LENGTH('e) > 1)" apply transfer apply (auto simp add: bias_def unat_mask_eq simp flip: mask_eq_exp_minus_1) apply (simp add: mask_eq_exp_minus_1) done end