src/HOL/Probability/Probability_Mass_Function.thy

   fixes A :: "'a set" and f :: "'a \<Rightarrow> 'b pmf"
     and  h :: "'b \<Rightarrow> 'c::{banach, second_countable_topology}"
   assumes "A \<noteq> {}" "finite A" "\<And>x. x \<in> A \<Longrightarrow> finite (set_pmf (f x))"
   shows "measure_pmf.expectation (pmf_of_set A \<bind> f) h =
            (\<Sum>a\<in>A. measure_pmf.expectation (f a) h /\<^sub>R real (card A))"
-  using assms by (subst pmf_expectation_bind[of A]) (auto simp: divide_simps)
+  using assms by (subst pmf_expectation_bind[of A]) (auto simp: field_split_simps)
 
 lemma map_pmf_of_set:
   assumes "finite A" "A \<noteq> {}"
   shows   "map_pmf f (pmf_of_set A) = pmf_of_multiset (image_mset f (mset_set A))"
     (is "?lhs = ?rhs")

   fix k
   have A: "indicator {Suc a} (Suc b) = indicator {a} b" for a b
     by (simp add: indicator_def)
   show "pmf (binomial_pmf (Suc n) p) k = pmf ?rhs k"
     by (cases k; cases "k > n")
-       (insert assms, auto simp: pmf_bind measure_pmf_single A divide_simps algebra_simps
+       (insert assms, auto simp: pmf_bind measure_pmf_single A field_split_simps algebra_simps
           not_less less_eq_Suc_le [symmetric] power_diff')
 qed
 
 lemma binomial_pmf_0: "p \<in> {0..1} \<Longrightarrow> binomial_pmf 0 p = return_pmf 0"
   by (rule pmf_eqI) (simp_all add: indicator_def)