--- a/src/HOL/Decision_Procs/Approximation_Bounds.thy Sat Feb 03 20:46:28 2018 +0100
+++ b/src/HOL/Decision_Procs/Approximation_Bounds.thy Mon Feb 05 08:30:19 2018 +0100
@@ -305,8 +305,7 @@
case (Float m e)
hence "0 < m"
using assms
- apply (auto simp: sign_simps)
- by (meson not_less powr_ge_pzero)
+ by (auto simp: sign_simps)
hence "0 < sqrt m" by auto
have int_nat_bl: "(nat (bitlen m)) = bitlen m"
@@ -1190,7 +1189,7 @@
next
case True
hence "x = 0"
- by transfer
+ by (simp add: real_of_float_eq)
thus ?thesis
using lb_sin_cos_aux_zero_le_one one_le_ub_sin_cos_aux
by simp
@@ -1478,7 +1477,7 @@
by auto
have eq_4: "?x2 * Float 1 (- 1) = x * Float 1 (- 2)"
- by transfer simp
+ by (auto simp: real_of_float_eq)
have "(?lb x) \<le> ?cos x"
proof -
@@ -2334,11 +2333,7 @@
using \<open>real_of_float (float_divr prec 1 x) < 1\<close> by auto
qed
-lemma float_pos_eq_mantissa_pos: "x > 0 \<longleftrightarrow> mantissa x > 0"
- apply (subst Float_mantissa_exponent[of x, symmetric])
- apply (auto simp add: zero_less_mult_iff zero_float_def dest: less_zeroE)
- apply (metis not_le powr_ge_pzero)
- done
+lemmas float_pos_eq_mantissa_pos = mantissa_pos_iff[symmetric]
lemma Float_pos_eq_mantissa_pos: "Float m e > 0 \<longleftrightarrow> m > 0"
using powr_gt_zero[of 2 "e"]
@@ -2346,7 +2341,7 @@
lemma Float_representation_aux:
fixes m e
- defines "x \<equiv> Float m e"
+ defines [THEN meta_eq_to_obj_eq]: "x \<equiv> Float m e"
assumes "x > 0"
shows "Float (exponent x + (bitlen (mantissa x) - 1)) 0 = Float (e + (bitlen m - 1)) 0" (is ?th1)
and "Float (mantissa x) (- (bitlen (mantissa x) - 1)) = Float m ( - (bitlen m - 1))" (is ?th2)
@@ -2356,9 +2351,10 @@
thus ?th1
using bitlen_Float[of m e] assms
by (auto simp add: zero_less_mult_iff intro!: arg_cong2[where f=Float])
- have "x \<noteq> float_of 0"
+ have "x \<noteq> 0"
unfolding zero_float_def[symmetric] using \<open>0 < x\<close> by auto
- from denormalize_shift[OF assms(1) this] guess i . note i = this
+ from denormalize_shift[OF x_def this] obtain i where
+ i: "m = mantissa x * 2 ^ i" "e = exponent x - int i" .
have "2 powr (1 - (real_of_int (bitlen (mantissa x)) + real_of_int i)) =
2 powr (1 - (real_of_int (bitlen (mantissa x)))) * inverse (2 powr (real i))"
@@ -2367,7 +2363,8 @@
(real_of_int (mantissa x) * 2 ^ i) * 2 powr (1 - real_of_int (bitlen (mantissa x * 2 ^ i)))"
using \<open>mantissa x > 0\<close> by (simp add: powr_realpow)
then show ?th2
- unfolding i by transfer auto
+ unfolding i
+ by (auto simp: real_of_float_eq)
qed
lemma compute_ln[code]:
@@ -2541,9 +2538,7 @@
let ?x = "Float m (- (bitlen m - 1))"
have "0 < m" and "m \<noteq> 0" using \<open>0 < x\<close> Float powr_gt_zero[of 2 e]
- apply (auto simp add: zero_less_mult_iff)
- using not_le powr_ge_pzero apply blast
- done
+ by (auto simp add: zero_less_mult_iff)
define bl where "bl = bitlen m - 1"
hence "bl \<ge> 0"
using \<open>m > 0\<close> by (simp add: bitlen_alt_def)
--- a/src/HOL/Library/Float.thy Sat Feb 03 20:46:28 2018 +0100
+++ b/src/HOL/Library/Float.thy Mon Feb 05 08:30:19 2018 +0100
@@ -300,8 +300,8 @@
"rel_fun (=) pcr_float (- numeral :: _ \<Rightarrow> real) (- numeral :: _ \<Rightarrow> float)"
by (simp add: rel_fun_def float.pcr_cr_eq cr_float_def)
-lemma float_of_numeral[simp]: "numeral k = float_of (numeral k)"
- and float_of_neg_numeral[simp]: "- numeral k = float_of (- numeral k)"
+lemma float_of_numeral: "numeral k = float_of (numeral k)"
+ and float_of_neg_numeral: "- numeral k = float_of (- numeral k)"
unfolding real_of_float_eq by simp_all
@@ -445,8 +445,8 @@
snd (SOME p::int \<times> int. (f = 0 \<and> fst p = 0 \<and> snd p = 0) \<or>
(f \<noteq> 0 \<and> real_of_float f = real_of_int (fst p) * 2 powr real_of_int (snd p) \<and> \<not> 2 dvd fst p))"
-lemma exponent_0[simp]: "exponent (float_of 0) = 0" (is ?E)
- and mantissa_0[simp]: "mantissa (float_of 0) = 0" (is ?M)
+lemma exponent_0[simp]: "exponent 0 = 0" (is ?E)
+ and mantissa_0[simp]: "mantissa 0 = 0" (is ?M)
proof -
have "\<And>p::int \<times> int. fst p = 0 \<and> snd p = 0 \<longleftrightarrow> p = (0, 0)"
by auto
@@ -455,13 +455,13 @@
qed
lemma mantissa_exponent: "real_of_float f = mantissa f * 2 powr exponent f" (is ?E)
- and mantissa_not_dvd: "f \<noteq> (float_of 0) \<Longrightarrow> \<not> 2 dvd mantissa f" (is "_ \<Longrightarrow> ?D")
+ and mantissa_not_dvd: "f \<noteq> 0 \<Longrightarrow> \<not> 2 dvd mantissa f" (is "_ \<Longrightarrow> ?D")
proof cases
- assume [simp]: "f \<noteq> float_of 0"
+ assume [simp]: "f \<noteq> 0"
have "f = mantissa f * 2 powr exponent f \<and> \<not> 2 dvd mantissa f"
proof (cases f rule: float_normed_cases)
case zero
- then show ?thesis by (simp add: zero_float_def)
+ then show ?thesis by simp
next
case (powr m e)
then have "\<exists>p::int \<times> int. (f = 0 \<and> fst p = 0 \<and> snd p = 0) \<or>
@@ -469,14 +469,37 @@
by auto
then show ?thesis
unfolding exponent_def mantissa_def
- by (rule someI2_ex) (simp add: zero_float_def)
+ by (rule someI2_ex) simp
qed
then show ?E ?D by auto
qed simp
-lemma mantissa_noteq_0: "f \<noteq> float_of 0 \<Longrightarrow> mantissa f \<noteq> 0"
+lemma mantissa_noteq_0: "f \<noteq> 0 \<Longrightarrow> mantissa f \<noteq> 0"
using mantissa_not_dvd[of f] by auto
+lemma mantissa_eq_zero_iff: "mantissa x = 0 \<longleftrightarrow> x = 0"
+ (is "?lhs \<longleftrightarrow> ?rhs")
+proof
+ show ?rhs if ?lhs
+ proof -
+ from that have z: "0 = real_of_float x"
+ using mantissa_exponent by simp
+ show ?thesis
+ by (simp add: zero_float_def z)
+ qed
+ show ?lhs if ?rhs
+ using that by simp
+qed
+
+lemma mantissa_pos_iff: "0 < mantissa x \<longleftrightarrow> 0 < x"
+ by (auto simp: mantissa_exponent sign_simps)
+
+lemma mantissa_nonneg_iff: "0 \<le> mantissa x \<longleftrightarrow> 0 \<le> x"
+ by (auto simp: mantissa_exponent sign_simps zero_le_mult_iff)
+
+lemma mantissa_neg_iff: "0 > mantissa x \<longleftrightarrow> 0 > x"
+ by (auto simp: mantissa_exponent sign_simps zero_le_mult_iff)
+
lemma
fixes m e :: int
defines "f \<equiv> float_of (m * 2 powr e)"
@@ -488,7 +511,7 @@
with dvd show "mantissa f = m" by auto
next
assume "m \<noteq> 0"
- then have f_not_0: "f \<noteq> float_of 0" by (simp add: f_def)
+ then have f_not_0: "f \<noteq> 0" by (simp add: f_def zero_float_def)
from mantissa_exponent[of f] have "m * 2 powr e = mantissa f * 2 powr exponent f"
by (auto simp add: f_def)
then show ?M ?E
@@ -509,8 +532,8 @@
by (atomize_elim) auto
lemma denormalize_shift:
- assumes f_def: "f \<equiv> Float m e"
- and not_0: "f \<noteq> float_of 0"
+ assumes f_def: "f = Float m e"
+ and not_0: "f \<noteq> 0"
obtains i where "m = mantissa f * 2 ^ i" "e = exponent f - i"
proof
from mantissa_exponent[of f] f_def
@@ -881,20 +904,20 @@
lemma bitlen_Float:
fixes m e
- defines "f \<equiv> Float m e"
+ defines [THEN meta_eq_to_obj_eq]: "f \<equiv> Float m e"
shows "bitlen \<bar>mantissa f\<bar> + exponent f = (if m = 0 then 0 else bitlen \<bar>m\<bar> + e)"
proof (cases "m = 0")
case True
- then show ?thesis by (simp add: f_def bitlen_alt_def Float_def)
+ then show ?thesis by (simp add: f_def bitlen_alt_def)
next
case False
- then have "f \<noteq> float_of 0"
+ then have "f \<noteq> 0"
unfolding real_of_float_eq by (simp add: f_def)
then have "mantissa f \<noteq> 0"
- by (simp add: mantissa_noteq_0)
+ by (simp add: mantissa_eq_zero_iff)
moreover
obtain i where "m = mantissa f * 2 ^ i" "e = exponent f - int i"
- by (rule f_def[THEN denormalize_shift, OF \<open>f \<noteq> float_of 0\<close>])
+ by (rule f_def[THEN denormalize_shift, OF \<open>f \<noteq> 0\<close>])
ultimately show ?thesis by (simp add: abs_mult)
qed
@@ -904,10 +927,7 @@
proof -
have "0 < Float m e" using assms by auto
then have "0 < m" using powr_gt_zero[of 2 e]
- apply (auto simp: zero_less_mult_iff)
- using not_le powr_ge_pzero
- apply blast
- done
+ by (auto simp: zero_less_mult_iff)
then have "m \<noteq> 0" by auto
show ?thesis
proof (cases "0 \<le> e")
@@ -1875,20 +1895,6 @@
lemma bitlen_1: "bitlen 1 = 1"
by (simp add: bitlen_alt_def)
-lemma mantissa_eq_zero_iff: "mantissa x = 0 \<longleftrightarrow> x = 0"
- (is "?lhs \<longleftrightarrow> ?rhs")
-proof
- show ?rhs if ?lhs
- proof -
- from that have z: "0 = real_of_float x"
- using mantissa_exponent by simp
- show ?thesis
- by (simp add: zero_float_def z)
- qed
- show ?lhs if ?rhs
- using that by (simp add: zero_float_def)
-qed
-
lemma float_upper_bound: "x \<le> 2 powr (bitlen \<bar>mantissa x\<bar> + exponent x)"
proof (cases "x = 0")
case True
@@ -2104,7 +2110,7 @@
by (simp add: truncate_up_eq_truncate_down truncate_down_mono)
lemma Float_le_zero_iff: "Float a b \<le> 0 \<longleftrightarrow> a \<le> 0"
- by (auto simp: zero_float_def mult_le_0_iff) (simp add: not_less [symmetric])
+ by (auto simp: zero_float_def mult_le_0_iff)
lemma real_of_float_pprt[simp]:
fixes a :: float
@@ -2147,7 +2153,7 @@
by transfer simp
lemma floor_pos_exp: "exponent (floor_fl x) \<ge> 0"
-proof (cases "floor_fl x = float_of 0")
+proof (cases "floor_fl x = 0")
case True
then show ?thesis
by (simp add: floor_fl_def)
@@ -2156,7 +2162,7 @@
have eq: "floor_fl x = Float \<lfloor>real_of_float x\<rfloor> 0"
by transfer simp
obtain i where "\<lfloor>real_of_float x\<rfloor> = mantissa (floor_fl x) * 2 ^ i" "0 = exponent (floor_fl x) - int i"
- by (rule denormalize_shift[OF eq[THEN eq_reflection] False])
+ by (rule denormalize_shift[OF eq False])
then show ?thesis
by simp
qed
@@ -2164,11 +2170,14 @@
lemma compute_mantissa[code]:
"mantissa (Float m e) =
(if m = 0 then 0 else if 2 dvd m then mantissa (normfloat (Float m e)) else m)"
- by (auto simp: mantissa_float Float.abs_eq)
+ by (auto simp: mantissa_float Float.abs_eq zero_float_def[symmetric])
lemma compute_exponent[code]:
"exponent (Float m e) =
(if m = 0 then 0 else if 2 dvd m then exponent (normfloat (Float m e)) else e)"
- by (auto simp: exponent_float Float.abs_eq)
+ by (auto simp: exponent_float Float.abs_eq zero_float_def[symmetric])
+
+lifting_update Float.float.lifting
+lifting_forget Float.float.lifting
end
--- a/src/HOL/Library/Log_Nat.thy Sat Feb 03 20:46:28 2018 +0100
+++ b/src/HOL/Library/Log_Nat.thy Mon Feb 05 08:30:19 2018 +0100
@@ -200,8 +200,11 @@
lemma bitlen_alt_def: "bitlen a = (if a > 0 then \<lfloor>log 2 a\<rfloor> + 1 else 0)"
by (simp add: bitlen_def floorlog_def)
+lemma bitlen_zero[simp]: "bitlen 0 = 0"
+ by (auto simp: bitlen_def floorlog_def)
+
lemma bitlen_nonneg: "0 \<le> bitlen x"
-by (simp add: bitlen_def)
+ by (simp add: bitlen_def)
lemma bitlen_bounds:
assumes "x > 0"
--- a/src/HOL/Matrix_LP/ComputeFloat.thy Sat Feb 03 20:46:28 2018 +0100
+++ b/src/HOL/Matrix_LP/ComputeFloat.thy Mon Feb 05 08:30:19 2018 +0100
@@ -188,11 +188,11 @@
lemma zero_le_float:
"(0 <= float (a,b)) = (0 <= a)"
- by (simp add: float_def zero_le_mult_iff) (simp add: not_less [symmetric])
+ by (simp add: float_def zero_le_mult_iff)
lemma float_le_zero:
"(float (a,b) <= 0) = (a <= 0)"
- by (simp add: float_def mult_le_0_iff) (simp add: not_less [symmetric])
+ by (simp add: float_def mult_le_0_iff)
lemma float_abs:
"\<bar>float (a,b)\<bar> = (if 0 <= a then (float (a,b)) else (float (-a,b)))"
--- a/src/HOL/Transcendental.thy Sat Feb 03 20:46:28 2018 +0100
+++ b/src/HOL/Transcendental.thy Mon Feb 05 08:30:19 2018 +0100
@@ -2495,6 +2495,9 @@
for x y :: real
by (simp add: powr_def)
+lemma powr_non_neg[simp]: "\<not>a powr x < 0" for a x::real
+ using powr_ge_pzero[of a x] by arith
+
lemma powr_divide: "0 < x \<Longrightarrow> 0 < y \<Longrightarrow> (x / y) powr a = (x powr a) / (y powr a)"
for a b x :: real
apply (simp add: divide_inverse positive_imp_inverse_positive powr_mult)
@@ -2606,6 +2609,10 @@
for a x :: real
by (simp add: powr_def)
+lemma powr_nonneg_iff[simp]: "a powr x \<le> 0 \<longleftrightarrow> a = 0"
+ for a x::real
+ by (meson not_less powr_gt_zero)
+
lemma log_add_eq_powr: "0 < b \<Longrightarrow> b \<noteq> 1 \<Longrightarrow> 0 < x \<Longrightarrow> log b x + y = log b (x * b powr y)"
and add_log_eq_powr: "0 < b \<Longrightarrow> b \<noteq> 1 \<Longrightarrow> 0 < x \<Longrightarrow> y + log b x = log b (b powr y * x)"
and log_minus_eq_powr: "0 < b \<Longrightarrow> b \<noteq> 1 \<Longrightarrow> 0 < x \<Longrightarrow> log b x - y = log b (x * b powr -y)"