src/HOL/Probability/PMF_Impl.thy

   using assms by transfer (auto split: option.splits)
 
 qualified lemma mapping_of_bind_pmf:
   assumes "finite (set_pmf p)"
   shows   "mapping_of_pmf (bind_pmf p f) = 
-             fold_combine_plus (\<lambda>x. Mapping.map_values (\<lambda>_. ( * ) (pmf p x)) 
+             fold_combine_plus (\<lambda>x. Mapping.map_values (\<lambda>_. (*) (pmf p x)) 
                (mapping_of_pmf (f x))) (set_pmf p)"
   using assms
   by (intro mapping_of_pmfI')
      (auto simp: keys_fold_combine_plus lookup_default_fold_combine_plus 
                  pmf_bind integral_measure_pmf lookup_default_0_map_values 

   by (intro mapping_of_pmfI') simp_all
 
 lemma bind_pmf_aux_code_aux:
   assumes "finite A"
   shows   "bind_pmf_aux p f A = 
-             fold_combine_plus (\<lambda>x. Mapping.map_values (\<lambda>_. ( * ) (pmf p x))
+             fold_combine_plus (\<lambda>x. Mapping.map_values (\<lambda>_. (*) (pmf p x))
                (mapping_of_pmf (f x))) A" (is "?lhs = ?rhs")
 proof (intro mapping_eqI'[where d = 0])
   fix x assume "x \<in> Mapping.keys ?lhs"
   then obtain y where y: "y \<in> A" "x \<in> set_pmf (f y)" by auto
   hence "Mapping.lookup_default 0 ?lhs x = 

   finally show "Mapping.lookup_default 0 ?lhs x = Mapping.lookup_default 0 ?rhs x" .
 qed (insert assms, simp_all add: keys_fold_combine_plus)
 
 lemma bind_pmf_aux_code [code]:
   "bind_pmf_aux p f (set xs) = 
-     fold_combine_plus (\<lambda>x. Mapping.map_values (\<lambda>_. ( * ) (pmf p x))
+     fold_combine_plus (\<lambda>x. Mapping.map_values (\<lambda>_. (*) (pmf p x))
                (mapping_of_pmf (f x))) (set xs)"
   by (rule bind_pmf_aux_code_aux) simp_all
 
 lemmas bind_pmf_code [code abstract] = bind_pmf_aux_correct