src/HOL/Probability/PMF_Impl.thy

 
 lemma pmf_of_multiset_impl_code_alt:
   assumes "A \<noteq> {#}"
   shows   "pmf_of_multiset_impl A =
              (let p = 1 / real (size A)
-              in  fold_mset (\<lambda>x. Mapping.map_default x 0 (op + p)) Mapping.empty A)"
+              in  fold_mset (\<lambda>x. Mapping.map_default x 0 ((+) p)) Mapping.empty A)"
 proof -
   define p where "p = 1 / real (size A)"
-  interpret comp_fun_commute "\<lambda>x. Mapping.map_default x 0 (op + p)"
+  interpret comp_fun_commute "\<lambda>x. Mapping.map_default x 0 ((+) p)"
     unfolding Mapping.map_default_def [abs_def]
     by (standard, intro mapping_eqI ext) 
        (simp_all add: o_def lookup_map_entry' lookup_default' lookup_default_def)
-  let ?m = "fold_mset (\<lambda>x. Mapping.map_default x 0 (op + p)) Mapping.empty A"
+  let ?m = "fold_mset (\<lambda>x. Mapping.map_default x 0 ((+) p)) Mapping.empty A"
   have keys: "Mapping.keys ?m = set_mset A" by (induction A) simp_all
   have lookup: "Mapping.lookup_default 0 ?m x = real (count A x) * p" for x
     by (induction A)
        (simp_all add: lookup_map_default' lookup_default_def lookup_empty ring_distribs)
   from keys lookup assms show ?thesis unfolding pmf_of_multiset_impl_def

   by transfer (auto simp: dom_def set_pmf_eq)
   
 
 
 definition fold_combine_plus where
-  "fold_combine_plus = comm_monoid_set.F (Mapping.combine (op + :: real \<Rightarrow> _)) Mapping.empty"
+  "fold_combine_plus = comm_monoid_set.F (Mapping.combine ((+) :: real \<Rightarrow> _)) Mapping.empty"
 
 context
 begin
 
-interpretation fold_combine_plus: combine_mapping_abel_semigroup "op + :: real \<Rightarrow> _"
+interpretation fold_combine_plus: combine_mapping_abel_semigroup "(+) :: real \<Rightarrow> _"
   by unfold_locales (simp_all add: add_ac)
   
 qualified lemma lookup_default_fold_combine_plus: 
   fixes A :: "'b set" and f :: "'b \<Rightarrow> ('a, real) mapping"
   assumes "finite A"

 qualified lemma keys_fold_combine_plus: 
   "finite A \<Longrightarrow> Mapping.keys (fold_combine_plus f A) = (\<Union>x\<in>A. Mapping.keys (f x))"
   by (simp add: fold_combine_plus_def fold_combine_plus.keys_fold_combine)
 
 qualified lemma fold_combine_plus_code [code]:
-  "fold_combine_plus g (set xs) = foldr (\<lambda>x. Mapping.combine op+ (g x)) (remdups xs) Mapping.empty"
+  "fold_combine_plus g (set xs) = foldr (\<lambda>x. Mapping.combine (+) (g x)) (remdups xs) Mapping.empty"
   by (simp add: fold_combine_plus_def fold_combine_plus.fold_combine_code)
 
 private lemma lookup_default_0_map_values:
   assumes "f x 0 = 0"
   shows   "Mapping.lookup_default 0 (Mapping.map_values f m) x = f x (Mapping.lookup_default 0 m x)"

   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>_. op * (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>_. op * (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>_. op * (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
 

   pmfify :: "('a::typerep multiset \<times> (unit \<Rightarrow> Code_Evaluation.term)) \<Rightarrow>
              'a \<times> (unit \<Rightarrow> Code_Evaluation.term) \<Rightarrow>
              'a pmf \<times> (unit \<Rightarrow> Code_Evaluation.term)" where
   [code_unfold]: "pmfify A x =  
     Code_Evaluation.valtermify pmf_of_multiset {\<cdot>} 
-      (Code_Evaluation.valtermify (op +) {\<cdot>} A {\<cdot>} 
+      (Code_Evaluation.valtermify (+) {\<cdot>} A {\<cdot>} 
        (Code_Evaluation.valtermify single {\<cdot>} x))"
 
 
 notation fcomp (infixl "\<circ>>" 60)
 notation scomp (infixl "\<circ>\<rightarrow>" 60)