src/HOL/Probability/SPMF.thy

   "ord_option ord x None"
   "ord_option ord (Some x) (Some y)"
   "ord_option ord (Some x) None"
 
 inductive_simps ord_option_eq_simps [simp]:
-  "ord_option op = None y"
-  "ord_option op = (Some x) y"
+  "ord_option (=) None y"
+  "ord_option (=) (Some x) y"
 
 lemma ord_option_reflI: "(\<And>y. y \<in> set_option x \<Longrightarrow> ord y y) \<Longrightarrow> ord_option ord x x"
 by(cases x) simp_all
 
 lemma reflp_ord_option: "reflp ord \<Longrightarrow> reflp (ord_option ord)"

   assumes lub_least: "\<And>Y y. \<lbrakk> Complete_Partial_Order.chain ord Y; \<And>x. x \<in> Y \<Longrightarrow> ord x y \<rbrakk> \<Longrightarrow> ord (lub Y) y"
   shows "ord_option ord (lub_option lub Y) y"
 using Y
 by(cases y)(auto 4 3 simp add: lub_option_def intro: lub_least[OF ord_option_chainD] dest: upper)
 
-lemma lub_map_option: "lub_option lub (map_option f ` Y) = lub_option (lub \<circ> op ` f) Y"
+lemma lub_map_option: "lub_option lub (map_option f ` Y) = lub_option (lub \<circ> (`) f) Y"
 apply(auto simp add: lub_option_def)
 apply(erule notE)
 apply(rule arg_cong[where f=lub])
 apply(auto intro: rev_image_eqI dest: sym)
 done

 
 context includes lifting_syntax
 begin
 
 definition rel_pred :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> 'b set \<Rightarrow> bool"
-where "rel_pred R A B = (R ===> op =) (\<lambda>x. x \<in> A) (\<lambda>y. y \<in> B)"
-
-lemma rel_predI: "(R ===> op =) (\<lambda>x. x \<in> A) (\<lambda>y. y \<in> B) \<Longrightarrow> rel_pred R A B"
+where "rel_pred R A B = (R ===> (=)) (\<lambda>x. x \<in> A) (\<lambda>y. y \<in> B)"
+
+lemma rel_predI: "(R ===> (=)) (\<lambda>x. x \<in> A) (\<lambda>y. y \<in> B) \<Longrightarrow> rel_pred R A B"
 by(simp add: rel_pred_def)
 
 lemma rel_predD: "\<lbrakk> rel_pred R A B; R x y \<rbrakk> \<Longrightarrow> x \<in> A \<longleftrightarrow> y \<in> B"
 by(simp add: rel_pred_def rel_fun_def)
 
-lemma Collect_parametric: "((A ===> op =) ===> rel_pred A) Collect Collect"
+lemma Collect_parametric: "((A ===> (=)) ===> rel_pred A) Collect Collect"
   \<comment> \<open>Declare this rule as @{attribute transfer_rule} only locally
       because it blows up the search space for @{method transfer}
       (in combination with @{thm [source] Collect_transfer})\<close>
 by(simp add: rel_funI rel_predI)
 
 end
 
 subsubsection \<open>Monotonicity rules\<close>
 
-lemma monotone_gfp_eadd1: "monotone op \<ge> op \<ge> (\<lambda>x. x + y :: enat)"
+lemma monotone_gfp_eadd1: "monotone (\<ge>) (\<ge>) (\<lambda>x. x + y :: enat)"
 by(auto intro!: monotoneI)
 
-lemma monotone_gfp_eadd2: "monotone op \<ge> op \<ge> (\<lambda>y. x + y :: enat)"
+lemma monotone_gfp_eadd2: "monotone (\<ge>) (\<ge>) (\<lambda>y. x + y :: enat)"
 by(auto intro!: monotoneI)
 
 lemma mono2mono_gfp_eadd[THEN gfp.mono2mono2, cont_intro, simp]:
-  shows monotone_eadd: "monotone (rel_prod op \<ge> op \<ge>) op \<ge> (\<lambda>(x, y). x + y :: enat)"
+  shows monotone_eadd: "monotone (rel_prod (\<ge>) (\<ge>)) (\<ge>) (\<lambda>(x, y). x + y :: enat)"
 by(simp add: monotone_gfp_eadd1 monotone_gfp_eadd2)
 
 lemma eadd_gfp_partial_function_mono [partial_function_mono]:
-  "\<lbrakk> monotone (fun_ord op \<ge>) op \<ge> f; monotone (fun_ord op \<ge>) op \<ge> g \<rbrakk>
-  \<Longrightarrow> monotone (fun_ord op \<ge>) op \<ge> (\<lambda>x. f x + g x :: enat)"
+  "\<lbrakk> monotone (fun_ord (\<ge>)) (\<ge>) f; monotone (fun_ord (\<ge>)) (\<ge>) g \<rbrakk>
+  \<Longrightarrow> monotone (fun_ord (\<ge>)) (\<ge>) (\<lambda>x. f x + g x :: enat)"
 by(rule mono2mono_gfp_eadd)
 
 lemma mono2mono_ereal[THEN lfp.mono2mono]:
-  shows monotone_ereal: "monotone op \<le> op \<le> ereal"
+  shows monotone_ereal: "monotone (\<le>) (\<le>) ereal"
 by(rule monotoneI) simp
 
 lemma mono2mono_ennreal[THEN lfp.mono2mono]:
-  shows monotone_ennreal: "monotone op \<le> op \<le> ennreal"
+  shows monotone_ennreal: "monotone (\<le>) (\<le>) ennreal"
 by(rule monotoneI)(simp add: ennreal_leI)
 
 subsubsection \<open>Bijections\<close>
 
 lemma bi_unique_rel_set_bij_betw:

 by(simp_all add: fun_eq_iff pmf.rel_map option.rel_map[abs_def])
 
 lemma spmf_rel_conversep: "rel_spmf R\<inverse>\<inverse> = (rel_spmf R)\<inverse>\<inverse>"
 by(simp add: option.rel_conversep pmf.rel_conversep)
 
-lemma spmf_rel_eq: "rel_spmf op = = op ="
+lemma spmf_rel_eq: "rel_spmf (=) = (=)"
 by(simp add: pmf.rel_eq option.rel_eq)
 
 context includes lifting_syntax
 begin
 

 
 lemma map_spmf_parametric: "((A ===> B) ===> rel_spmf A ===> rel_spmf B) map_spmf map_spmf"
 by transfer_prover
 
 lemma rel_spmf_parametric:
-  "((A ===> B ===> op =) ===> rel_spmf A ===> rel_spmf B ===> op =) rel_spmf rel_spmf"
+  "((A ===> B ===> (=)) ===> rel_spmf A ===> rel_spmf B ===> (=)) rel_spmf rel_spmf"
 by transfer_prover
 
 lemma set_spmf_parametric [transfer_rule]:
   "(rel_spmf A ===> rel_set A) set_spmf set_spmf"
 unfolding set_spmf_def[abs_def] by transfer_prover

 context includes lifting_syntax
 begin
 
 text \<open>We do not yet have a relator for @{typ "'a measure"}, so we combine @{const measure} and @{const measure_pmf}\<close>
 lemma measure_pmf_parametric:
-  "(rel_pmf A ===> rel_pred A ===> op =) (\<lambda>p. measure (measure_pmf p)) (\<lambda>q. measure (measure_pmf q))"
+  "(rel_pmf A ===> rel_pred A ===> (=)) (\<lambda>p. measure (measure_pmf p)) (\<lambda>q. measure (measure_pmf q))"
 proof(rule rel_funI)+
   fix p q X Y
   assume "rel_pmf A p q" and "rel_pred A X Y"
   from this(1) obtain pq where A: "\<And>x y. (x, y) \<in> set_pmf pq \<Longrightarrow> A x y"
     and p: "p = map_pmf fst pq" and q: "q = map_pmf snd pq" by cases auto
   show "measure p X = measure q Y" unfolding p q measure_map_pmf
     by(rule measure_pmf.finite_measure_eq_AE)(auto simp add: AE_measure_pmf_iff dest!: A rel_predD[OF \<open>rel_pred _ _ _\<close>])
 qed
 
 lemma measure_spmf_parametric:
-  "(rel_spmf A ===> rel_pred A ===> op =) (\<lambda>p. measure (measure_spmf p)) (\<lambda>q. measure (measure_spmf q))"
+  "(rel_spmf A ===> rel_pred A ===> (=)) (\<lambda>p. measure (measure_spmf p)) (\<lambda>q. measure (measure_spmf q))"
 unfolding measure_measure_spmf_conv_measure_pmf[abs_def]
 apply(rule rel_funI)+
 apply(erule measure_pmf_parametric[THEN rel_funD, THEN rel_funD])
 apply(auto simp add: rel_pred_def rel_fun_def elim: option.rel_cases)
 done

                ennreal (pmf pq (None, Some y)) * indicator {None} x \<partial>count_space UNIV)"
         by(rule nn_integral_cong)(auto split: split_indicator)
       also have "\<dots> = (\<integral>\<^sup>+ x. ennreal (pmf pq (x, Some y)) * indicator (range Some) x \<partial>count_space UNIV) + pmf pq (None, Some y)"
         by(subst nn_integral_add)(simp_all)
       also have "\<dots> = (\<integral>\<^sup>+ x. ennreal (spmf p y) * indicator {Some y} x \<partial>count_space UNIV) + (spmf q y - spmf p y)"
-        by(auto simp add: pq_def pmf_embed_pmf[OF f] one_ereal_def[symmetric] simp del: nn_integral_indicator_singleton intro!: arg_cong2[where f="op +"] nn_integral_cong split: option.split)
+        by(auto simp add: pq_def pmf_embed_pmf[OF f] one_ereal_def[symmetric] simp del: nn_integral_indicator_singleton intro!: arg_cong2[where f="(+)"] nn_integral_cong split: option.split)
       also have "\<dots> = spmf q y" by(simp add: ennreal_minus[symmetric] le)
       finally show ?thesis using Some by simp
     qed
     finally show "pmf (map_pmf snd pq) i = pmf q i" by simp
   qed
 qed
 
 lemma ord_spmf_eq_leD:
-  assumes "ord_spmf op = p q"
+  assumes "ord_spmf (=) p q"
   shows "spmf p x \<le> spmf q x"
 proof(cases "x \<in> set_spmf p")
   case False
   thus ?thesis by(simp add: in_set_spmf_iff_spmf)
 next
   case True
   from assms obtain pq
-    where pq: "\<And>x y. (x, y) \<in> set_pmf pq \<Longrightarrow> ord_option op = x y"
+    where pq: "\<And>x y. (x, y) \<in> set_pmf pq \<Longrightarrow> ord_option (=) x y"
     and p: "p = map_pmf fst pq"
     and q: "q = map_pmf snd pq" by cases auto
   have "ennreal (spmf p x) = integral\<^sup>N pq (indicator (fst -` {Some x}))"
     using p by(simp add: ennreal_pmf_map)
   also have "\<dots> = integral\<^sup>N pq (indicator {(Some x, Some x)})"

     by(rule nn_integral_mono) simp
   also have "\<dots> = ennreal (spmf q x)" using q by(simp add: ennreal_pmf_map)
   finally show ?thesis by simp
 qed
 
-lemma ord_spmf_eqD_set_spmf: "ord_spmf op = p q \<Longrightarrow> set_spmf p \<subseteq> set_spmf q"
+lemma ord_spmf_eqD_set_spmf: "ord_spmf (=) p q \<Longrightarrow> set_spmf p \<subseteq> set_spmf q"
 by(rule subsetI)(drule_tac x=x in ord_spmf_eq_leD, auto simp add: in_set_spmf_iff_spmf)
 
 lemma ord_spmf_eqD_emeasure:
-  "ord_spmf op = p q \<Longrightarrow> emeasure (measure_spmf p) A \<le> emeasure (measure_spmf q) A"
+  "ord_spmf (=) p q \<Longrightarrow> emeasure (measure_spmf p) A \<le> emeasure (measure_spmf q) A"
 by(auto intro!: nn_integral_mono split: split_indicator dest: ord_spmf_eq_leD simp add: nn_integral_measure_spmf nn_integral_indicator[symmetric])
 
-lemma ord_spmf_eqD_measure_spmf: "ord_spmf op = p q \<Longrightarrow> measure_spmf p \<le> measure_spmf q"
+lemma ord_spmf_eqD_measure_spmf: "ord_spmf (=) p q \<Longrightarrow> measure_spmf p \<le> measure_spmf q"
   by (subst le_measure) (auto simp: ord_spmf_eqD_emeasure)
 
-subsection \<open>CCPO structure for the flat ccpo @{term "ord_option op ="}\<close>
+subsection \<open>CCPO structure for the flat ccpo @{term "ord_option (=)"}\<close>
 
 context fixes Y :: "'a spmf set" begin
 
 definition lub_spmf :: "'a spmf"
 where "lub_spmf = embed_spmf (\<lambda>x. enn2real (SUP p : Y. ennreal (spmf p x)))"
   \<comment> \<open>We go through @{typ ennreal} to have a sensible definition even if @{term Y} is empty.\<close>
 
 lemma lub_spmf_empty [simp]: "SPMF.lub_spmf {} = return_pmf None"
 by(simp add: SPMF.lub_spmf_def bot_ereal_def)
 
-context assumes chain: "Complete_Partial_Order.chain (ord_spmf op =) Y" begin
-
-lemma chain_ord_spmf_eqD: "Complete_Partial_Order.chain (op \<le>) ((\<lambda>p x. ennreal (spmf p x)) ` Y)"
+context assumes chain: "Complete_Partial_Order.chain (ord_spmf (=)) Y" begin
+
+lemma chain_ord_spmf_eqD: "Complete_Partial_Order.chain (\<le>) ((\<lambda>p x. ennreal (spmf p x)) ` Y)"
   (is "Complete_Partial_Order.chain _ (?f ` _)")
 proof(rule chainI)
   fix f g
   assume "f \<in> ?f ` Y" "g \<in> ?f ` Y"
   then obtain p q where f: "f = ?f p" "p \<in> Y" and g: "g = ?f q" "q \<in> Y" by blast
-  from chain \<open>p \<in> Y\<close> \<open>q \<in> Y\<close> have "ord_spmf op = p q \<or> ord_spmf op = q p" by(rule chainD)
+  from chain \<open>p \<in> Y\<close> \<open>q \<in> Y\<close> have "ord_spmf (=) p q \<or> ord_spmf (=) q p" by(rule chainD)
   thus "f \<le> g \<or> g \<le> f"
   proof
-    assume "ord_spmf op = p q"
+    assume "ord_spmf (=) p q"
     hence "\<And>x. spmf p x \<le> spmf q x" by(rule ord_spmf_eq_leD)
     hence "f \<le> g" unfolding f g by(auto intro: le_funI)
     thus ?thesis ..
   next
-    assume "ord_spmf op = q p"
+    assume "ord_spmf (=) q p"
     hence "\<And>x. spmf q x \<le> spmf p x" by(rule ord_spmf_eq_leD)
     hence "g \<le> f" unfolding f g by(auto intro: le_funI)
     thus ?thesis ..
   qed
 qed
 
 lemma ord_spmf_eq_pmf_None_eq:
-  assumes le: "ord_spmf op = p q"
+  assumes le: "ord_spmf (=) p q"
   and None: "pmf p None = pmf q None"
   shows "p = q"
 proof(rule spmf_eqI)
   fix i
   from le have le': "\<And>x. spmf p x \<le> spmf q x" by(rule ord_spmf_eq_leD)

     by(simp add: nn_integral_0_iff_AE AE_count_space ennreal_minus ennreal_eq_0_iff)
   with le' show "spmf p i = spmf q i" by(rule antisym)
 qed
 
 lemma ord_spmf_eqD_pmf_None:
-  assumes "ord_spmf op = x y"
+  assumes "ord_spmf (=) x y"
   shows "pmf x None \<ge> pmf y None"
 using assms
 apply cases
 apply(clarsimp simp only: ennreal_le_iff[symmetric, OF pmf_nonneg] ennreal_pmf_map)
 apply(fastforce simp add: AE_measure_pmf_iff intro!: nn_integral_mono_AE)

 \<close>
 lemma spmf_chain_countable: "countable (\<Union>p\<in>Y. set_spmf p)"
 proof(cases "Y = {}")
   case Y: False
   show ?thesis
-  proof(cases "\<exists>x\<in>Y. \<forall>y\<in>Y. ord_spmf op = y x")
+  proof(cases "\<exists>x\<in>Y. \<forall>y\<in>Y. ord_spmf (=) y x")
     case True
-    then obtain x where x: "x \<in> Y" and upper: "\<And>y. y \<in> Y \<Longrightarrow> ord_spmf op = y x" by blast
+    then obtain x where x: "x \<in> Y" and upper: "\<And>y. y \<in> Y \<Longrightarrow> ord_spmf (=) y x" by blast
     hence "(\<Union>x\<in>Y. set_spmf x) \<subseteq> set_spmf x" by(auto dest: ord_spmf_eqD_set_spmf)
     thus ?thesis by(rule countable_subset) simp
   next
     case False
     define N :: "'a option pmf \<Rightarrow> real" where "N p = pmf p None" for p
 
-    have N_less_imp_le_spmf: "\<lbrakk> x \<in> Y; y \<in> Y; N y < N x \<rbrakk> \<Longrightarrow> ord_spmf op = x y" for x y
+    have N_less_imp_le_spmf: "\<lbrakk> x \<in> Y; y \<in> Y; N y < N x \<rbrakk> \<Longrightarrow> ord_spmf (=) x y" for x y
       using chainD[OF chain, of x y] ord_spmf_eqD_pmf_None[of x y] ord_spmf_eqD_pmf_None[of y x]
       by (auto simp: N_def)
     have N_eq_imp_eq: "\<lbrakk> x \<in> Y; y \<in> Y; N y = N x \<rbrakk> \<Longrightarrow> x = y" for x y
       using chainD[OF chain, of x y] by(auto simp add: N_def dest: ord_spmf_eq_pmf_None_eq)
 

     proof(rule ccontr)
       assume **: "\<not> (\<exists>y\<in>N ` Y. y < N x)"
       { fix y
         assume "y \<in> Y"
         with ** consider "N x < N y" | "N x = N y" by(auto simp add: not_less le_less)
-        hence "ord_spmf op = y x" using \<open>y \<in> Y\<close> \<open>x \<in> Y\<close>
+        hence "ord_spmf (=) y x" using \<open>y \<in> Y\<close> \<open>x \<in> Y\<close>
           by cases(auto dest: N_less_imp_le_spmf N_eq_imp_eq intro: ord_spmf_reflI) }
       with False \<open>x \<in> Y\<close> show False by blast
     qed
 
     from NC have "Inf (N ` Y) \<in> closure (N ` Y)" by (intro closure_contains_Inf)

 lemma ennreal_spmf_lub_spmf: "Y \<noteq> {} \<Longrightarrow> ennreal (spmf lub_spmf x) = (SUP p:Y. ennreal (spmf p x))"
 unfolding spmf_lub_spmf by(subst ennreal_SUP)(simp_all add: SUP_spmf_neq_top' del: SUP_eq_top_iff Sup_eq_top_iff)
 
 lemma lub_spmf_upper:
   assumes p: "p \<in> Y"
-  shows "ord_spmf op = p lub_spmf"
+  shows "ord_spmf (=) p lub_spmf"
 proof(rule ord_pmf_increaseI)
   fix x
   from p have [simp]: "Y \<noteq> {}" by auto
   from p have "ennreal (spmf p x) \<le> (SUP p:Y. ennreal (spmf p x))" by(rule SUP_upper)
   also have "\<dots> = ennreal (spmf lub_spmf x)" using p
     by(subst spmf_lub_spmf)(auto simp add: ennreal_SUP SUP_spmf_neq_top' simp del: SUP_eq_top_iff Sup_eq_top_iff)
   finally show "spmf p x \<le> spmf lub_spmf x" by simp
 qed simp
 
 lemma lub_spmf_least:
-  assumes z: "\<And>x. x \<in> Y \<Longrightarrow> ord_spmf op = x z"
-  shows "ord_spmf op = lub_spmf z"
+  assumes z: "\<And>x. x \<in> Y \<Longrightarrow> ord_spmf (=) x z"
+  shows "ord_spmf (=) lub_spmf z"
 proof(cases "Y = {}")
   case nonempty: False
   show ?thesis
   proof(rule ord_pmf_increaseI)
     fix x

     by(simp add: spmf_lub_spmf assms ennreal_SUP[OF SUP_spmf_neq_top'] SUP_mult_right_ennreal)
   also from assms have "\<dots> = (SUP y:Y. \<integral>\<^sup>+ x. ennreal (spmf y x) * indicator A x \<partial>?M)"
   proof(rule nn_integral_monotone_convergence_SUP_countable)
     have "(\<lambda>i x. ennreal (spmf i x) * indicator A x) ` Y = (\<lambda>f x. f x * indicator A x) ` (\<lambda>p x. ennreal (spmf p x)) ` Y"
       by(simp add: image_image)
-    also have "Complete_Partial_Order.chain op \<le> \<dots>" using chain_ord_spmf_eqD
+    also have "Complete_Partial_Order.chain (\<le>) \<dots>" using chain_ord_spmf_eqD
       by(rule chain_imageI)(auto simp add: le_fun_def split: split_indicator)
-    finally show "Complete_Partial_Order.chain op \<le> ((\<lambda>i x. ennreal (spmf i x) * indicator A x) ` Y)" .
+    finally show "Complete_Partial_Order.chain (\<le>) ((\<lambda>i x. ennreal (spmf i x) * indicator A x) ` Y)" .
   qed simp
   also have "\<dots> = (SUP y:Y. \<integral>\<^sup>+ x. ennreal (spmf y x) * indicator A x \<partial>count_space UNIV)"
     by(auto simp add: nn_integral_count_space_indicator set_lub_spmf spmf_eq_0_set_spmf split: split_indicator intro!: SUP_cong nn_integral_cong)
   also have "\<dots> = ?rhs"
     by(auto simp add: nn_integral_indicator[symmetric] nn_integral_measure_spmf)

 lemma measure_spmf_lub_spmf:
   assumes Y: "Y \<noteq> {}"
   shows "measure_spmf lub_spmf = (SUP p:Y. measure_spmf p)" (is "?lhs = ?rhs")
 proof(rule measure_eqI)
   from assms obtain p where p: "p \<in> Y" by auto
-  from chain have chain': "Complete_Partial_Order.chain op \<le> (measure_spmf ` Y)"
+  from chain have chain': "Complete_Partial_Order.chain (\<le>) (measure_spmf ` Y)"
     by(rule chain_imageI)(rule ord_spmf_eqD_measure_spmf)
   show "sets ?lhs = sets ?rhs"
     using Y by (subst sets_SUP) auto
   show "emeasure ?lhs A = emeasure ?rhs A" for A
     using chain' Y p by (subst emeasure_SUP_chain) (auto simp:  emeasure_lub_spmf)

 
 end
 
 end
 
-lemma partial_function_definitions_spmf: "partial_function_definitions (ord_spmf op =) lub_spmf"
+lemma partial_function_definitions_spmf: "partial_function_definitions (ord_spmf (=)) lub_spmf"
   (is "partial_function_definitions ?R _")
 proof
   fix x show "?R x x" by(simp add: ord_spmf_reflI)
 next
   fix x y z

   assume "Complete_Partial_Order.chain ?R Y" "\<And>x. x \<in> Y \<Longrightarrow> ?R x z"
   then show "?R (lub_spmf Y) z"
     by(cases "Y = {}")(simp_all add: lub_spmf_least)
 qed
 
-lemma ccpo_spmf: "class.ccpo lub_spmf (ord_spmf op =) (mk_less (ord_spmf op =))"
+lemma ccpo_spmf: "class.ccpo lub_spmf (ord_spmf (=)) (mk_less (ord_spmf (=)))"
 by(rule ccpo partial_function_definitions_spmf)+
 
-interpretation spmf: partial_function_definitions "ord_spmf op =" "lub_spmf"
+interpretation spmf: partial_function_definitions "ord_spmf (=)" "lub_spmf"
   rewrites "lub_spmf {} \<equiv> return_pmf None"
 by(rule partial_function_definitions_spmf) simp
 
 declaration \<open>Partial_Function.init "spmf" @{term spmf.fixp_fun}
   @{term spmf.mono_body} @{thm spmf.fixp_rule_uc} @{thm spmf.fixp_induct_uc}
   NONE\<close>
 
 declare spmf.leq_refl[simp]
 declare admissible_leI[OF ccpo_spmf, cont_intro]
 
-abbreviation "mono_spmf \<equiv> monotone (fun_ord (ord_spmf op =)) (ord_spmf op =)"
+abbreviation "mono_spmf \<equiv> monotone (fun_ord (ord_spmf (=))) (ord_spmf (=))"
 
 lemma lub_spmf_const [simp]: "lub_spmf {p} = p"
 by(rule spmf_eqI)(simp add: spmf_lub_spmf[OF ccpo.chain_singleton[OF ccpo_spmf]])
 
 lemma bind_spmf_mono':
-  assumes fg: "ord_spmf op = f g"
-  and hk: "\<And>x :: 'a. ord_spmf op = (h x) (k x)"
-  shows "ord_spmf op = (f \<bind> h) (g \<bind> k)"
+  assumes fg: "ord_spmf (=) f g"
+  and hk: "\<And>x :: 'a. ord_spmf (=) (h x) (k x)"
+  shows "ord_spmf (=) (f \<bind> h) (g \<bind> k)"
 unfolding bind_spmf_def using assms(1)
 by(rule rel_pmf_bindI)(auto split: option.split simp add: hk)
 
 lemma bind_spmf_mono [partial_function_mono]:
   assumes mf: "mono_spmf B" and mg: "\<And>y. mono_spmf (\<lambda>f. C y f)"
   shows "mono_spmf (\<lambda>f. bind_spmf (B f) (\<lambda>y. C y f))"
 proof (rule monotoneI)
   fix f g :: "'a \<Rightarrow> 'b spmf"
-  assume fg: "fun_ord (ord_spmf op =) f g"
-  with mf have "ord_spmf op = (B f) (B g)" by (rule monotoneD[of _ _ _ f g])
-  moreover from mg have "\<And>y'. ord_spmf op = (C y' f) (C y' g)"
+  assume fg: "fun_ord (ord_spmf (=)) f g"
+  with mf have "ord_spmf (=) (B f) (B g)" by (rule monotoneD[of _ _ _ f g])
+  moreover from mg have "\<And>y'. ord_spmf (=) (C y' f) (C y' g)"
     by (rule monotoneD) (rule fg)
-  ultimately show "ord_spmf op = (bind_spmf (B f) (\<lambda>y. C y f)) (bind_spmf (B g) (\<lambda>y'. C y' g))"
+  ultimately show "ord_spmf (=) (bind_spmf (B f) (\<lambda>y. C y f)) (bind_spmf (B g) (\<lambda>y'. C y' g))"
     by(rule bind_spmf_mono')
 qed
 
-lemma monotone_bind_spmf1: "monotone (ord_spmf op =) (ord_spmf op =) (\<lambda>y. bind_spmf y g)"
+lemma monotone_bind_spmf1: "monotone (ord_spmf (=)) (ord_spmf (=)) (\<lambda>y. bind_spmf y g)"
 by(rule monotoneI)(simp add: bind_spmf_mono' ord_spmf_reflI)
 
 lemma monotone_bind_spmf2:
-  assumes g: "\<And>x. monotone ord (ord_spmf op =) (\<lambda>y. g y x)"
-  shows "monotone ord (ord_spmf op =) (\<lambda>y. bind_spmf p (g y))"
+  assumes g: "\<And>x. monotone ord (ord_spmf (=)) (\<lambda>y. g y x)"
+  shows "monotone ord (ord_spmf (=)) (\<lambda>y. bind_spmf p (g y))"
 by(rule monotoneI)(auto intro: bind_spmf_mono' monotoneD[OF g] ord_spmf_reflI)
 
 lemma bind_lub_spmf:
-  assumes chain: "Complete_Partial_Order.chain (ord_spmf op =) Y"
+  assumes chain: "Complete_Partial_Order.chain (ord_spmf (=)) Y"
   shows "bind_spmf (lub_spmf Y) f = lub_spmf ((\<lambda>p. bind_spmf p f) ` Y)" (is "?lhs = ?rhs")
 proof(cases "Y = {}")
   case Y: False
   show ?thesis
   proof(rule spmf_eqI)
     fix i
-    have chain': "Complete_Partial_Order.chain op \<le> ((\<lambda>p x. ennreal (spmf p x * spmf (f x) i)) ` Y)"
+    have chain': "Complete_Partial_Order.chain (\<le>) ((\<lambda>p x. ennreal (spmf p x * spmf (f x) i)) ` Y)"
       using chain by(rule chain_imageI)(auto simp add: le_fun_def dest: ord_spmf_eq_leD intro: mult_right_mono)
-    have chain'': "Complete_Partial_Order.chain (ord_spmf op =) ((\<lambda>p. p \<bind> f) ` Y)"
+    have chain'': "Complete_Partial_Order.chain (ord_spmf (=)) ((\<lambda>p. p \<bind> f) ` Y)"
       using chain by(rule chain_imageI)(auto intro!: monotoneI bind_spmf_mono' ord_spmf_reflI)
     let ?M = "count_space (set_spmf (lub_spmf Y))"
     have "ennreal (spmf ?lhs i) = \<integral>\<^sup>+ x. ennreal (spmf (lub_spmf Y) x) * ennreal (spmf (f x) i) \<partial>?M"
       by(auto simp add: ennreal_spmf_lub_spmf ennreal_spmf_bind nn_integral_measure_spmf')
     also have "\<dots> = \<integral>\<^sup>+ x. (SUP p:Y. ennreal (spmf p x * spmf (f x) i)) \<partial>?M"

     finally show "spmf ?lhs i = spmf ?rhs i" by simp
   qed
 qed simp
 
 lemma map_lub_spmf:
-  "Complete_Partial_Order.chain (ord_spmf op =) Y
+  "Complete_Partial_Order.chain (ord_spmf (=)) Y
   \<Longrightarrow> map_spmf f (lub_spmf Y) = lub_spmf (map_spmf f ` Y)"
 unfolding map_spmf_conv_bind_spmf[abs_def] by(simp add: bind_lub_spmf o_def)
 
-lemma mcont_bind_spmf1: "mcont lub_spmf (ord_spmf op =) lub_spmf (ord_spmf op =) (\<lambda>y. bind_spmf y f)"
+lemma mcont_bind_spmf1: "mcont lub_spmf (ord_spmf (=)) lub_spmf (ord_spmf (=)) (\<lambda>y. bind_spmf y f)"
 using monotone_bind_spmf1 by(rule mcontI)(rule contI, simp add: bind_lub_spmf)
 
 lemma bind_lub_spmf2:
   assumes chain: "Complete_Partial_Order.chain ord Y"
-  and g: "\<And>y. monotone ord (ord_spmf op =) (g y)"
+  and g: "\<And>y. monotone ord (ord_spmf (=)) (g y)"
   shows "bind_spmf x (\<lambda>y. lub_spmf (g y ` Y)) = lub_spmf ((\<lambda>p. bind_spmf x (\<lambda>y. g y p)) ` Y)"
   (is "?lhs = ?rhs")
 proof(cases "Y = {}")
   case Y: False
   show ?thesis
   proof(rule spmf_eqI)
     fix i
-    have chain': "\<And>y. Complete_Partial_Order.chain (ord_spmf op =) (g y ` Y)"
+    have chain': "\<And>y. Complete_Partial_Order.chain (ord_spmf (=)) (g y ` Y)"
       using chain g[THEN monotoneD] by(rule chain_imageI)
-    have chain'': "Complete_Partial_Order.chain op \<le> ((\<lambda>p y. ennreal (spmf x y * spmf (g y p) i)) ` Y)"
+    have chain'': "Complete_Partial_Order.chain (\<le>) ((\<lambda>p y. ennreal (spmf x y * spmf (g y p) i)) ` Y)"
       using chain by(rule chain_imageI)(auto simp add: le_fun_def dest: ord_spmf_eq_leD monotoneD[OF g] intro!: mult_left_mono)
-    have chain''': "Complete_Partial_Order.chain (ord_spmf op =) ((\<lambda>p. bind_spmf x (\<lambda>y. g y p)) ` Y)"
+    have chain''': "Complete_Partial_Order.chain (ord_spmf (=)) ((\<lambda>p. bind_spmf x (\<lambda>y. g y p)) ` Y)"
       using chain by(rule chain_imageI)(rule monotone_bind_spmf2[OF g, THEN monotoneD])
 
     have "ennreal (spmf ?lhs i) = \<integral>\<^sup>+ y. (SUP p:Y. ennreal (spmf x y * spmf (g y p) i)) \<partial>count_space (set_spmf x)"
       by(simp add: ennreal_spmf_bind ennreal_spmf_lub_spmf[OF chain'] Y nn_integral_measure_spmf' SUP_mult_left_ennreal ennreal_mult)
     also have "\<dots> = (SUP p:Y. \<integral>\<^sup>+ y. ennreal (spmf x y * spmf (g y p) i) \<partial>count_space (set_spmf x))"

     finally show "spmf ?lhs i = spmf ?rhs i" by simp
   qed
 qed simp
 
 lemma mcont_bind_spmf [cont_intro]:
-  assumes f: "mcont luba orda lub_spmf (ord_spmf op =) f"
-  and g: "\<And>y. mcont luba orda lub_spmf (ord_spmf op =) (g y)"
-  shows "mcont luba orda lub_spmf (ord_spmf op =) (\<lambda>x. bind_spmf (f x) (\<lambda>y. g y x))"
+  assumes f: "mcont luba orda lub_spmf (ord_spmf (=)) f"
+  and g: "\<And>y. mcont luba orda lub_spmf (ord_spmf (=)) (g y)"
+  shows "mcont luba orda lub_spmf (ord_spmf (=)) (\<lambda>x. bind_spmf (f x) (\<lambda>y. g y x))"
 proof(rule spmf.mcont2mcont'[OF _ _ f])
   fix z
-  show "mcont lub_spmf (ord_spmf op =) lub_spmf (ord_spmf op =) (\<lambda>x. bind_spmf x (\<lambda>y. g y z))"
+  show "mcont lub_spmf (ord_spmf (=)) lub_spmf (ord_spmf (=)) (\<lambda>x. bind_spmf x (\<lambda>y. g y z))"
     by(rule mcont_bind_spmf1)
 next
   fix x
   let ?f = "\<lambda>z. bind_spmf x (\<lambda>y. g y z)"
-  have "monotone orda (ord_spmf op =) ?f" using mcont_mono[OF g] by(rule monotone_bind_spmf2)
-  moreover have "cont luba orda lub_spmf (ord_spmf op =) ?f"
+  have "monotone orda (ord_spmf (=)) ?f" using mcont_mono[OF g] by(rule monotone_bind_spmf2)
+  moreover have "cont luba orda lub_spmf (ord_spmf (=)) ?f"
   proof(rule contI)
     fix Y
     assume chain: "Complete_Partial_Order.chain orda Y" and Y: "Y \<noteq> {}"
     have "bind_spmf x (\<lambda>y. g y (luba Y)) = bind_spmf x (\<lambda>y. lub_spmf (g y ` Y))"
       by(rule bind_spmf_cong)(simp_all add: mcont_contD[OF g chain Y])
     also have "\<dots> = lub_spmf ((\<lambda>p. x \<bind> (\<lambda>y. g y p)) ` Y)" using chain
       by(rule bind_lub_spmf2)(rule mcont_mono[OF g])
     finally show "bind_spmf x (\<lambda>y. g y (luba Y)) = \<dots>" .
   qed
-  ultimately show "mcont luba orda lub_spmf (ord_spmf op =) ?f" by(rule mcontI)
+  ultimately show "mcont luba orda lub_spmf (ord_spmf (=)) ?f" by(rule mcontI)
 qed
 
 lemma bind_pmf_mono [partial_function_mono]:
   "(\<And>y. mono_spmf (\<lambda>f. C y f)) \<Longrightarrow> mono_spmf (\<lambda>f. bind_pmf p (\<lambda>x. C x f))"
 using bind_spmf_mono[of "\<lambda>_. spmf_of_pmf p" C] by simp
 
 lemma map_spmf_mono [partial_function_mono]: "mono_spmf B \<Longrightarrow> mono_spmf (\<lambda>g. map_spmf f (B g))"
 unfolding map_spmf_conv_bind_spmf by(rule bind_spmf_mono) simp_all
 
 lemma mcont_map_spmf [cont_intro]:
-  "mcont luba orda lub_spmf (ord_spmf op =) g
-  \<Longrightarrow> mcont luba orda lub_spmf (ord_spmf op =) (\<lambda>x. map_spmf f (g x))"
+  "mcont luba orda lub_spmf (ord_spmf (=)) g
+  \<Longrightarrow> mcont luba orda lub_spmf (ord_spmf (=)) (\<lambda>x. map_spmf f (g x))"
 unfolding map_spmf_conv_bind_spmf by(rule mcont_bind_spmf) simp_all
 
-lemma monotone_set_spmf: "monotone (ord_spmf op =) op \<subseteq> set_spmf"
+lemma monotone_set_spmf: "monotone (ord_spmf (=)) (\<subseteq>) set_spmf"
 by(rule monotoneI)(rule ord_spmf_eqD_set_spmf)
 
-lemma cont_set_spmf: "cont lub_spmf (ord_spmf op =) Union op \<subseteq> set_spmf"
+lemma cont_set_spmf: "cont lub_spmf (ord_spmf (=)) Union (\<subseteq>) set_spmf"
 by(rule contI)(subst set_lub_spmf; simp)
 
 lemma mcont2mcont_set_spmf[THEN mcont2mcont, cont_intro]:
-  shows mcont_set_spmf: "mcont lub_spmf (ord_spmf op =) Union op \<subseteq> set_spmf"
+  shows mcont_set_spmf: "mcont lub_spmf (ord_spmf (=)) Union (\<subseteq>) set_spmf"
 by(rule mcontI monotone_set_spmf cont_set_spmf)+
 
-lemma monotone_spmf: "monotone (ord_spmf op =) op \<le> (\<lambda>p. spmf p x)"
+lemma monotone_spmf: "monotone (ord_spmf (=)) (\<le>) (\<lambda>p. spmf p x)"
 by(rule monotoneI)(simp add: ord_spmf_eq_leD)
 
-lemma cont_spmf: "cont lub_spmf (ord_spmf op =) Sup op \<le> (\<lambda>p. spmf p x)"
+lemma cont_spmf: "cont lub_spmf (ord_spmf (=)) Sup (\<le>) (\<lambda>p. spmf p x)"
 by(rule contI)(simp add: spmf_lub_spmf)
 
-lemma mcont_spmf: "mcont lub_spmf (ord_spmf op =) Sup op \<le> (\<lambda>p. spmf p x)"
+lemma mcont_spmf: "mcont lub_spmf (ord_spmf (=)) Sup (\<le>) (\<lambda>p. spmf p x)"
 by(rule mcontI monotone_spmf cont_spmf)+
 
-lemma cont_ennreal_spmf: "cont lub_spmf (ord_spmf op =) Sup op \<le> (\<lambda>p. ennreal (spmf p x))"
+lemma cont_ennreal_spmf: "cont lub_spmf (ord_spmf (=)) Sup (\<le>) (\<lambda>p. ennreal (spmf p x))"
 by(rule contI)(simp add: ennreal_spmf_lub_spmf)
 
 lemma mcont2mcont_ennreal_spmf [THEN mcont2mcont, cont_intro]:
-  shows mcont_ennreal_spmf: "mcont lub_spmf (ord_spmf op =) Sup op \<le> (\<lambda>p. ennreal (spmf p x))"
+  shows mcont_ennreal_spmf: "mcont lub_spmf (ord_spmf (=)) Sup (\<le>) (\<lambda>p. ennreal (spmf p x))"
 by(rule mcontI mono2mono_ennreal monotone_spmf cont_ennreal_spmf)+
 
 lemma nn_integral_map_spmf [simp]: "nn_integral (measure_spmf (map_spmf f p)) g = nn_integral (measure_spmf p) (g \<circ> f)"
 by(auto 4 3 simp add: measure_spmf_def nn_integral_distr nn_integral_restrict_space intro: nn_integral_cong split: split_indicator)
 

       (auto 4 3 intro!: arg_cong2[where f=measure] simp add: option_rel_Some1 option_rel_Some2 A'_def intro: rev_bexI elim: option.rel_cases)
   finally show "measure (measure_pmf p) A \<le> \<dots>" .
 qed
 
 lemma admissible_rel_spmf:
-  "ccpo.admissible (prod_lub lub_spmf lub_spmf) (rel_prod (ord_spmf op =) (ord_spmf op =)) (case_prod (rel_spmf R))"
+  "ccpo.admissible (prod_lub lub_spmf lub_spmf) (rel_prod (ord_spmf (=)) (ord_spmf (=))) (case_prod (rel_spmf R))"
   (is "ccpo.admissible ?lub ?ord ?P")
 proof(rule ccpo.admissibleI)
   fix Y
   assume chain: "Complete_Partial_Order.chain ?ord Y"
     and Y: "Y \<noteq> {}"
     and R: "\<forall>(p, q) \<in> Y. rel_spmf R p q"
   from R have R: "\<And>p q. (p, q) \<in> Y \<Longrightarrow> rel_spmf R p q" by auto
-  have chain1: "Complete_Partial_Order.chain (ord_spmf op =) (fst ` Y)"
-    and chain2: "Complete_Partial_Order.chain (ord_spmf op =) (snd ` Y)"
+  have chain1: "Complete_Partial_Order.chain (ord_spmf (=)) (fst ` Y)"
+    and chain2: "Complete_Partial_Order.chain (ord_spmf (=)) (snd ` Y)"
     using chain by(rule chain_imageI; clarsimp)+
   from Y have Y1: "fst ` Y \<noteq> {}" and Y2: "snd ` Y \<noteq> {}" by auto
 
   have "rel_spmf R (lub_spmf (fst ` Y)) (lub_spmf (snd ` Y))"
   proof(rule rel_spmf_measureI)

   qed
   then show "?P (?lub Y)" by(simp add: prod_lub_def)
 qed
 
 lemma admissible_rel_spmf_mcont [cont_intro]:
-  "\<lbrakk> mcont lub ord lub_spmf (ord_spmf op =) f; mcont lub ord lub_spmf (ord_spmf op =) g \<rbrakk>
+  "\<lbrakk> mcont lub ord lub_spmf (ord_spmf (=)) f; mcont lub ord lub_spmf (ord_spmf (=)) g \<rbrakk>
   \<Longrightarrow> ccpo.admissible lub ord (\<lambda>x. rel_spmf R (f x) (g x))"
 by(rule admissible_subst[OF admissible_rel_spmf, where f="\<lambda>x. (f x, g x)", simplified])(rule mcont_Pair)
 
 context includes lifting_syntax
 begin
 
 lemma fixp_spmf_parametric':
-  assumes f: "\<And>x. monotone (ord_spmf op =) (ord_spmf op =) F"
-  and g: "\<And>x. monotone (ord_spmf op =) (ord_spmf op =) G"
+  assumes f: "\<And>x. monotone (ord_spmf (=)) (ord_spmf (=)) F"
+  and g: "\<And>x. monotone (ord_spmf (=)) (ord_spmf (=)) G"
   and param: "(rel_spmf R ===> rel_spmf R) F G"
-  shows "(rel_spmf R) (ccpo.fixp lub_spmf (ord_spmf op =) F) (ccpo.fixp lub_spmf (ord_spmf op =) G)"
+  shows "(rel_spmf R) (ccpo.fixp lub_spmf (ord_spmf (=)) F) (ccpo.fixp lub_spmf (ord_spmf (=)) G)"
 by(rule parallel_fixp_induct[OF ccpo_spmf ccpo_spmf _ f g])(auto intro: param[THEN rel_funD])
 
 lemma fixp_spmf_parametric:
   assumes f: "\<And>x. mono_spmf (\<lambda>f. F f x)"
   and g: "\<And>x. mono_spmf (\<lambda>f. G f x)"
   and param: "((A ===> rel_spmf R) ===> A ===> rel_spmf R) F G"
   shows "(A ===> rel_spmf R) (spmf.fixp_fun F) (spmf.fixp_fun G)"
 using f g
 proof(rule parallel_fixp_induct_1_1[OF partial_function_definitions_spmf partial_function_definitions_spmf _ _ reflexive reflexive, where P="(A ===> rel_spmf R)"])
-  show "ccpo.admissible (prod_lub (fun_lub lub_spmf) (fun_lub lub_spmf)) (rel_prod (fun_ord (ord_spmf op =)) (fun_ord (ord_spmf op =))) (\<lambda>x. (A ===> rel_spmf R) (fst x) (snd x))"
+  show "ccpo.admissible (prod_lub (fun_lub lub_spmf) (fun_lub lub_spmf)) (rel_prod (fun_ord (ord_spmf (=))) (fun_ord (ord_spmf (=)))) (\<lambda>x. (A ===> rel_spmf R) (fst x) (snd x))"
     unfolding rel_fun_def
     apply(rule admissible_all admissible_imp admissible_rel_spmf_mcont)+
     apply(rule spmf.mcont2mcont[OF mcont_call])
      apply(rule mcont_fst)
     apply(rule spmf.mcont2mcont[OF mcont_call])

 qed
 
 abbreviation coin_spmf :: "bool spmf"
 where "coin_spmf \<equiv> spmf_of_set UNIV"
 
-lemma map_eq_const_coin_spmf: "map_spmf (op = c) coin_spmf = coin_spmf"
-proof -
-  have "inj (op \<longleftrightarrow> c)" "range (op \<longleftrightarrow> c) = UNIV" by(auto intro: inj_onI)
+lemma map_eq_const_coin_spmf: "map_spmf ((=) c) coin_spmf = coin_spmf"
+proof -
+  have "inj ((\<longleftrightarrow>) c)" "range ((\<longleftrightarrow>) c) = UNIV" by(auto intro: inj_onI)
   then show ?thesis by simp
 qed
 
 lemma bind_coin_spmf_eq_const: "coin_spmf \<bind> (\<lambda>x :: bool. return_spmf (b = x)) = coin_spmf"
 using map_eq_const_coin_spmf unfolding map_spmf_conv_bind_spmf by simp

 lemma assumes "rel_spmf (\<lambda>x y. bad1 x = bad2 y \<and> (\<not> bad2 y \<longrightarrow> A x \<longleftrightarrow> B y)) p q" (is "rel_spmf ?A _ _")
   shows fundamental_lemma_bad: "measure (measure_spmf p) {x. bad1 x} = measure (measure_spmf q) {y. bad2 y}" (is "?bad")
   and fundamental_lemma: "\<bar>measure (measure_spmf p) {x. A x} - measure (measure_spmf q) {y. B y}\<bar> \<le>
     measure (measure_spmf p) {x. bad1 x}" (is ?fundamental)
 proof -
-  have good: "rel_fun ?A op = (\<lambda>x. A x \<and> \<not> bad1 x) (\<lambda>y. B y \<and> \<not> bad2 y)" by(auto simp add: rel_fun_def)
+  have good: "rel_fun ?A (=) (\<lambda>x. A x \<and> \<not> bad1 x) (\<lambda>y. B y \<and> \<not> bad2 y)" by(auto simp add: rel_fun_def)
   from assms have 1: "measure (measure_spmf p) {x. A x \<and> \<not> bad1 x} = measure (measure_spmf q) {y. B y \<and> \<not> bad2 y}"
     by(rule measure_spmf_parametric[THEN rel_funD, THEN rel_funD])(rule Collect_parametric[THEN rel_funD, OF good])
 
-  have bad: "rel_fun ?A op = bad1 bad2" by(simp add: rel_fun_def)
+  have bad: "rel_fun ?A (=) bad1 bad2" by(simp add: rel_fun_def)
   show 2: ?bad using assms
     by(rule measure_spmf_parametric[THEN rel_funD, THEN rel_funD])(rule Collect_parametric[THEN rel_funD, OF bad])
 
   let ?\<mu>p = "measure (measure_spmf p)" and ?\<mu>q = "measure (measure_spmf q)"
   have "{x. A x \<and> bad1 x} \<union> {x. A x \<and> \<not> bad1 x} = {x. A x}"