--- a/src/HOL/Library/Float.thy Mon Aug 26 22:14:19 2024 +0100
+++ b/src/HOL/Library/Float.thy Fri Aug 30 10:16:48 2024 +0100
@@ -103,8 +103,8 @@
by (simp add: float_def) (metis mult_minus_left of_int_minus)
lemma times_float[simp]: "x \<in> float \<Longrightarrow> y \<in> float \<Longrightarrow> x * y \<in> float"
- apply (clarsimp simp: float_def)
- by (metis (no_types, opaque_lifting) of_int_add powr_add mult.assoc mult.left_commute of_int_mult)
+ apply (clarsimp simp: float_def mult_ac)
+ by (metis mult.assoc of_int_mult of_int_add powr_add)
lemma minus_float[simp]: "x \<in> float \<Longrightarrow> y \<in> float \<Longrightarrow> x - y \<in> float"
using plus_float [of x "- y"] by simp
@@ -248,10 +248,7 @@
end
lemma float_numeral[simp]: "real_of_float (numeral x :: float) = numeral x"
-proof (induct x)
- case One
- then show ?case by simp
-qed (metis of_int_numeral real_of_float_of_int_eq)+
+ by (metis of_int_numeral real_of_float_of_int_eq)
lemma transfer_numeral [transfer_rule]:
"rel_fun (=) pcr_float (numeral :: _ \<Rightarrow> real) (numeral :: _ \<Rightarrow> float)"
@@ -525,10 +522,7 @@
then have "mantissa f = m * 2^nat (e - exponent f)"
by linarith
with \<open>exponent f < e\<close> have "2 dvd mantissa f"
- apply (intro dvdI[where k="m * 2^(nat (e-exponent f)) div 2"])
- apply (cases "nat (e - exponent f)")
- apply auto
- done
+ by (force intro: dvdI[where k="m * 2^(nat (e-exponent f)) div 2"])
then show False using mantissa_not_dvd[OF not_0] by simp
qed
ultimately have "real_of_int m = mantissa f * 2^nat (exponent f - e)"
@@ -843,15 +837,7 @@
then have ne: "real_of_int (a mod b) / real_of_int b \<noteq> 0"
using \<open>b \<noteq> 0\<close> by auto
have "\<lceil>real_of_int a / real_of_int b\<rceil> = \<lfloor>real_of_int a / real_of_int b\<rfloor> + 1"
- apply (rule ceiling_eq)
- apply (auto simp flip: floor_divide_of_int_eq)
- proof -
- have "real_of_int \<lfloor>real_of_int a / real_of_int b\<rfloor> \<le> real_of_int a / real_of_int b"
- by simp
- moreover have "real_of_int \<lfloor>real_of_int a / real_of_int b\<rfloor> \<noteq> real_of_int a / real_of_int b"
- by (smt (verit) floor_divide_of_int_eq ne of_int_div_aux)
- ultimately show "real_of_int \<lfloor>real_of_int a / real_of_int b\<rfloor> < real_of_int a / real_of_int b" by arith
- qed
+ by (metis add_cancel_left_right ceiling_altdef floor_divide_of_int_eq ne of_int_div_aux)
then show ?thesis
using \<open>\<not> b dvd a\<close> by simp
qed
@@ -967,11 +953,12 @@
proof -
have "0 \<le> log 2 x - real_of_int \<lfloor>log 2 x\<rfloor>"
by (simp add: algebra_simps)
- with assms
- show ?thesis
- apply (auto simp: truncate_down_def round_down_def mult_powr_eq
+ moreover have "0 \<le> real p - real_of_int \<lfloor>log 2 x\<rfloor> + log 2 x"
+ by linarith
+ ultimately show ?thesis
+ using assms
+ by (auto simp: truncate_down_def round_down_def mult_powr_eq
intro!: ge_one_powr_ge_zero mult_pos_pos)
- by linarith
qed
lemma truncate_down_nonneg: "0 \<le> y \<Longrightarrow> 0 \<le> truncate_down prec y"
@@ -2119,8 +2106,7 @@
assume [simp]: "odd j"
have "power_up prec 0 (Suc (j div 2)) \<le> - power_up prec b (Suc (j div 2))"
if "b < 0" "even (j div 2)"
- apply (rule order_trans[where y=0])
- using IH that by (auto simp: div2_less_self)
+ by (metis Suc_neq_Zero even_Suc neg_0_le_iff_le power_up_eq_zero_iff power_up_nonpos_iff that)
then have "truncate_up prec ((power_up prec a (Suc (j div 2)))\<^sup>2)
\<le> truncate_up prec ((power_up prec b (Suc (j div 2)))\<^sup>2)"
using IH
@@ -2307,9 +2293,7 @@
qualified lemma compute_floor_fl[code]:
"floor_fl (Float m e) = (if 0 \<le> e then Float m e else Float (m div (2 ^ (nat (-e)))) 0)"
apply transfer
- apply (simp add: powr_int floor_divide_of_int_eq)
- apply (metis floor_divide_of_int_eq of_int_eq_numeral_power_cancel_iff)
- done
+ using compute_int_floor_fl int_floor_fl.rep_eq powr_int by auto
end