diff -r 94bc8f62c835 -r 07c51801c2ea src/HOL/Library/Float.thy
--- 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