src/HOL/Analysis/Improper_Integral.thy

     qed
   next
     case False
     have prod_if: "(\<Prod>k\<in>Basis \<inter> - {i}. f k) = (\<Prod>k\<in>Basis. f k) / f i" if "f i \<noteq> (0::real)" for f
       using that mk_disjoint_insert [OF i]
-      apply (clarsimp simp add: divide_simps)
+      apply (clarsimp simp add: field_split_simps)
       by (metis Int_insert_left_if0 finite_Basis finite_insert le_iff_inf mult.commute order_refl prod.insert subset_Compl_singleton)
     have abc: "a \<bullet> i < c" "c < b \<bullet> i"
       using False assms by auto
     then have "(\<Sum>K\<in>\<D>. ((\<lambda>K. content K / (interval_upperbound K \<bullet> i - interval_lowerbound K \<bullet> i)) \<circ> ((\<lambda>K. K \<inter> {x. x \<bullet> i \<le> c}))) K)
                   \<le> content(cbox a b') / (c - a \<bullet> i)"
               "(\<Sum>K\<in>\<D>. ((\<lambda>K. content K / (interval_upperbound K \<bullet> i - interval_lowerbound K \<bullet> i)) \<circ> ((\<lambda>K. K \<inter> {x. x \<bullet> i \<ge> c}))) K)
                  \<le> content(cbox a' b) / (b \<bullet> i - c)"
-      using lec gec by (simp_all add: divide_simps mult.commute)
+      using lec gec by (simp_all add: field_split_simps mult.commute)
     moreover
     have "(\<Sum>K\<in>\<D>. content K / (interval_upperbound K \<bullet> i - interval_lowerbound K \<bullet> i))
           \<le> (\<Sum>K\<in>\<D>. ((\<lambda>K. content K / (interval_upperbound K \<bullet> i - interval_lowerbound K \<bullet> i)) \<circ> ((\<lambda>K. K \<inter> {x. x \<bullet> i \<le> c}))) K) +
             (\<Sum>K\<in>\<D>. ((\<lambda>K. content K / (interval_upperbound K \<bullet> i - interval_lowerbound K \<bullet> i)) \<circ> ((\<lambda>K. K \<inter> {x. x \<bullet> i \<ge> c}))) K)"
            (is "?lhs \<le> ?rhs")

     ultimately
     have "(\<Sum>K\<in>\<D>. content K / (interval_upperbound K \<bullet> i - interval_lowerbound K \<bullet> i))
           \<le> 2 * content (cbox a b) / (b \<bullet> i - a \<bullet> i)"
       by linarith
     then show ?thesis
-      using abc by (simp add: divide_simps mult.commute)
+      using abc by (simp add: field_split_simps mult.commute)
   qed
 qed
 
 
 

   define \<gamma> where "\<gamma> \<equiv> \<lambda>x. \<gamma>0 x \<inter>
                           ball x ((\<epsilon>/8 / (norm(f x) + 1)) * (INF m\<in>Basis. b \<bullet> m - a \<bullet> m) / content(cbox a b))"
   have "gauge (\<lambda>x. ball x
                     (\<epsilon> * (INF m\<in>Basis. b \<bullet> m - a \<bullet> m) / ((8 * norm (f x) + 8) * content (cbox a b))))"
     using \<open>0 < content (cbox a b)\<close> \<open>0 < \<epsilon>\<close> a_less_b
-    apply (auto simp: gauge_def divide_simps mult_less_0_iff zero_less_mult_iff add_nonneg_eq_0_iff finite_less_Inf_iff)
-    apply (meson add_nonneg_nonneg mult_nonneg_nonneg norm_ge_zero not_less zero_le_numeral)
+    apply (auto simp: gauge_def field_split_simps mult_less_0_iff zero_less_mult_iff add_nonneg_eq_0_iff finite_less_Inf_iff)
+    apply (meson add_increasing measure_nonneg mult_nonneg_nonneg norm_ge_zero not_le zero_le_numeral)
     done
   then have "gauge \<gamma>"
     unfolding \<gamma>_def using \<open>gauge \<gamma>0\<close> gauge_Int by auto
   moreover
   have "(\<Sum>(x,K) \<in> S. norm (integral K h)) < \<epsilon>"

               using x that by (auto simp: norm_f)
             also have "... < (norm (f x) + 1)"
               by simp
             also have "... < \<epsilon> * (b \<bullet> i - a \<bullet> i) / dist u v / (4 * content (cbox a b))"
               using duv dist_uv contab_gt0
-              apply (simp add: divide_simps algebra_simps mult_less_0_iff zero_less_mult_iff split: if_split_asm)
+              apply (simp add: field_split_simps algebra_simps mult_less_0_iff zero_less_mult_iff split: if_split_asm)
               by (meson add_nonneg_nonneg linorder_not_le measure_nonneg mult_nonneg_nonneg norm_ge_zero zero_le_numeral)
             also have "... = \<epsilon> * (b \<bullet> i - a \<bullet> i) / norm (v - u) / (4 * content (cbox a b))"
               by (simp add: dist_norm norm_minus_commute)
             also have "... \<le> \<epsilon> * (b \<bullet> i - a \<bullet> i) / \<bar>v \<bullet> i - u \<bullet> i\<bar> / (4 * content (cbox a b))"
               apply (intro mult_right_mono divide_left_mono divide_right_mono uvi)

           qed
           with Kgt0 have "norm (content K *\<^sub>R h x) \<le> content K * ((\<epsilon>/4 * (b \<bullet> i - a \<bullet> i) / content (cbox a b)) / ?\<Delta>)"
             using mult_left_mono by fastforce
           also have "... = \<epsilon>/4 * (b \<bullet> i - a \<bullet> i) / content (cbox a b) *
                            content K / ?\<Delta>"
-            by (simp add: divide_simps)
+            by (simp add: field_split_simps)
           finally show ?thesis .
         qed
       qed
       also have "... = (\<Sum>K\<in>snd ` S. \<epsilon>/4 * (b \<bullet> i - a \<bullet> i) / content (cbox a b) * content K
                                      / (interval_upperbound K \<bullet> i - interval_lowerbound K \<bullet> i))"

               by (metis (full_types) order_trans Basis_le_norm inner_commute inner_diff_right that)
             show "1/n < \<bar>x \<bullet> i - c \<bullet> i\<bar>" "1/n < \<bar>x \<bullet> i - d \<bullet> i\<bar>"
               using n \<open>n \<noteq> 0\<close> emin [OF \<open>i \<in> Basis\<close>]
               by (simp_all add: inverse_eq_divide)
             show "1 / real (Suc m) \<le> 1 / real n"
-              using \<open>n \<noteq> 0\<close> \<open>m \<ge> n\<close> by (simp add: divide_simps)
+              using \<open>n \<noteq> 0\<close> \<open>m \<ge> n\<close> by (simp add: field_split_simps)
           qed
           then show ?thesis by (simp add: mem_box)
         qed
         then show ?thesis by blast
       qed

             using le_imp_inverse_le [OF * \<Delta>]
             by (simp add: field_simps)
           with N have "k > ((b - a) \<bullet> i) / ((x - a) \<bullet> i)"
             using \<open>N \<le> k\<close> by linarith
           with x that show ?thesis
-            by (auto simp: mem_box algebra_simps divide_simps)
+            by (auto simp: mem_box algebra_simps field_split_simps)
         qed
         have bx_gt: "(b - x) \<bullet> i > ((b - a) \<bullet> i) / k" if "i \<in> Basis" for i
         proof -
           have *: "Inf ?\<Delta> \<le> ((b - x) \<bullet> i) / ((b - a) \<bullet> i)"
             using that by (force intro: cInf_le_finite)

             using le_imp_inverse_le [OF * \<Delta>]
             by (simp add: field_simps)
           with N have "k > ((b - a) \<bullet> i) / ((b - x) \<bullet> i)"
             using \<open>N \<le> k\<close> by linarith
           with x that show ?thesis
-            by (auto simp: mem_box algebra_simps divide_simps)
+            by (auto simp: mem_box algebra_simps field_split_simps)
         qed
         show "x \<in> cbox (a + (b - a) /\<^sub>R k) (b - (b - a) /\<^sub>R k)"
           using that \<Delta> \<open>k > 0\<close>
           by (auto simp: mem_box algebra_simps divide_inverse dest: xa_gt bx_gt)
       qed

   have "n * f x \<ge> 0"
     using assms by auto
   then obtain m::nat where m: "floor(n * f x) = int m"
     using nonneg_int_cases zero_le_floor by blast
   then have kn: "real k / real n \<le> f x \<longleftrightarrow> k \<le> m" for k
-    using \<open>n \<noteq> 0\<close> by (simp add: divide_simps mult.commute) linarith
+    using \<open>n \<noteq> 0\<close> by (simp add: field_split_simps mult.commute) linarith
   then have "Suc n / real n \<le> f x \<longleftrightarrow> Suc n \<le> m"
     by blast
   have "real n * f x \<le> real n"
     by (simp add: \<open>x \<in> S\<close> f mult_left_le)
   then have "m \<le> n"
     using m by linarith
   have "?lhs = \<bar>f x - (\<Sum>k \<in> {Suc 0..n} \<inter> {..m}. inverse n)\<bar>"
     by (subst sum.inter_restrict) (auto simp: kn)
   also have "\<dots> < inverse n"
     using \<open>m \<le> n\<close> \<open>n \<noteq> 0\<close> m
-    by (simp add: min_absorb2 divide_simps mult.commute) linarith
+    by (simp add: min_absorb2 field_split_simps mult.commute) linarith
   finally show ?thesis .
 qed
 
 
 lemma SMVT_lemma2:

             proof (rule level_approx [of "{a..b}" g])
               show "\<sigma> n \<noteq> 0"
                 by (metis Suc_n_not_le_n non0)
             qed (use x 01 non0 in auto)
             also have "\<dots> \<le> inverse N"
-              using seq_suble [OF \<sigma>] \<open>N \<noteq> 0\<close> non0 that by (auto intro: order_trans simp: divide_simps)
+              using seq_suble [OF \<sigma>] \<open>N \<noteq> 0\<close> non0 that by (auto intro: order_trans simp: field_split_simps)
             finally show ?thesis
               by linarith
           qed
           ultimately show "\<exists>N. \<forall>n\<ge>N. \<bar>\<psi> n x - g x\<bar> < e"
             using less_trans by blast

         using \<open>a \<le> c\<close> \<open>c \<le> b\<close> by auto
       have I: "((\<lambda>x. g x * f x - g a * f x) has_integral (g b - g a) * integral {c..b} f) {a..b}"
       proof (subst has_integral_cong)
         show "g x * f x - g a * f x = (g b - g a) * h x *\<^sub>R f x"
           if "x \<in> {a..b}" for x
-          using 1 that by (simp add: h_def divide_simps algebra_simps)
+          using 1 that by (simp add: h_def field_split_simps algebra_simps)
         show "((\<lambda>x. (g b - g a) * h x *\<^sub>R f x) has_integral (g b - g a) * integral {c..b} f) {a..b}"
           using has_integral_mult_right [OF c, of "g b - g a"] .
       qed
       have II: "((\<lambda>x. g a * f x) has_integral g a * integral {a..b} f) {a..b}"
         using has_integral_mult_right [where c = "g a", OF integrable_integral [OF f]] .