src/HOL/Decision_Procs/Approximation.thy

 lemma ln_shifted_float:
   assumes "0 < m"
   shows "ln (Float m e) = ln 2 * (e + (bitlen m - 1)) + ln (Float m (- (bitlen m - 1)))"
 proof -
   let ?B = "2^nat (bitlen m - 1)"
-  def bl \<equiv> "bitlen m - 1"
+  define bl where "bl = bitlen m - 1"
   have "0 < real_of_int m" and "\<And>X. (0 :: real) < 2^X" and "0 < (2 :: real)" and "m \<noteq> 0"
     using assms by auto
   hence "0 \<le> bl" by (simp add: bitlen_def bl_def)
   show ?thesis
   proof (cases "0 \<le> e")

   case False
   hence "\<not> x \<le> 0" and "\<not> x < 1" "0 < x" "\<not> x \<le> Float 3 (- 1)"
     using \<open>1 \<le> x\<close> by auto
   show ?thesis
   proof -
-    def m \<equiv> "mantissa x"
-    def e \<equiv> "exponent x"
+    define m where "m = mantissa x"
+    define e where "e = exponent x"
     from Float_mantissa_exponent[of x] have Float: "x = Float m e"
       by (simp add: m_def e_def)
     let ?s = "Float (e + (bitlen m - 1)) 0"
     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
-    def bl \<equiv> "bitlen m - 1"
+    define bl where "bl = bitlen m - 1"
     hence "bl \<ge> 0"
       using \<open>m > 0\<close> by (simp add: bitlen_def)
     have "1 \<le> Float m e"
       using \<open>1 \<le> x\<close> Float unfolding less_eq_float_def by auto
     from bitlen_div[OF \<open>0 < m\<close>] float_gt1_scale[OF \<open>1 \<le> Float m e\<close>] \<open>bl \<ge> 0\<close>

   proof cases
     assume "l1 = 0" "u1 = 0"
     with x lu show ?thesis by (auto simp: bnds_powr_def)
   next
     assume A: "l1 = 0" "u1 \<noteq> 0" "l2 \<ge> 1"
-    def uln \<equiv> "the (ub_ln prec u1)"
+    define uln where "uln = the (ub_ln prec u1)"
     show ?thesis
     proof (cases "x = 0")
       case False
       with A x y have "x powr y = exp (ln x * y)" by (simp add: powr_def)
       also {

     hence setprod_head_Suc: "\<And>k i. \<Prod>{k ..< k + Suc i} = k * \<Prod>{Suc k ..< Suc k + i}"
       by auto
     have setsum_move0: "\<And>k F. setsum F {0..<Suc k} = F 0 + setsum (\<lambda> k. F (Suc k)) {0..<k}"
       unfolding setsum_shift_bounds_Suc_ivl[symmetric]
       unfolding setsum_head_upt_Suc[OF zero_less_Suc] ..
-    def C \<equiv> "xs!x - c"
+    define C where "C = xs!x - c"
 
     {
       fix t::real assume t: "t \<in> {lx .. ux}"
       hence "bounded_by [xs!x] [vs!x]"
         using \<open>bounded_by xs vs\<close>[THEN bounded_byE, OF \<open>x < length vs\<close>]

     and bnd_c: "real_of_float c \<in> {lx .. ux}"
     and "x < length vs" and "x < length xs"
     and ate: "Some (l, u) = approx_tse prec x s c 1 f vs"
   shows "interpret_floatarith f xs \<in> {l .. u}"
 proof -
-  def F \<equiv> "\<lambda>n z. interpret_floatarith ((DERIV_floatarith x ^^ n) f) (xs[x := z])"
+  define F where [abs_def]: "F n z =
+    interpret_floatarith ((DERIV_floatarith x ^^ n) f) (xs[x := z])" for n z
   hence F0: "F 0 = (\<lambda> z. interpret_floatarith f (xs[x := z]))" by auto
 
   hence "bounded_by (xs[x := c]) vs" and "x < length vs" "x < length xs"
     using \<open>bounded_by xs vs\<close> bnd_x bnd_c \<open>x < length vs\<close> \<open>x < length xs\<close>
     by (auto intro!: bounded_by_update_var)