src/HOL/BNF/More_BNFs.thy

 imports
   Basic_BNFs
   "~~/src/HOL/Library/FSet"
   "~~/src/HOL/Library/Multiset"
 begin
+
+notation
+  ordLeq2 (infix "<=o" 50) and
+  ordLeq3 (infix "\<le>o" 50) and
+  ordLess2 (infix "<o" 50) and
+  ordIso2 (infix "=o" 50) and
+  csum (infixr "+c" 65) and
+  cprod (infixr "*c" 80) and
+  cexp (infixr "^c" 90) and
+  convol ("<_ , _>")
 
 lemma option_rec_conv_option_case: "option_rec = option_case"
 by (simp add: fun_eq_iff split: option.split)
 
 bnf "'a option"

   fix x f g
   assume "\<And>z. z \<in> set x \<Longrightarrow> f z = g z"
   thus "map f x = map g x" by simp
 next
   fix f
-  show "set o map f = image f o set" by (rule ext, unfold o_apply, rule set_map)
+  show "set o map f = image f o set" by (rule ext, unfold comp_apply, rule set_map)
 next
   show "card_order natLeq" by (rule natLeq_card_order)
 next
   show "cinfinite natLeq" by (rule natLeq_cinfinite)
 next

   also have "... = setsum (setsum (count f) o ?As) ?B"
     by(intro setsum_reindex) (auto simp add: setsum_gt_0_iff inj_on_def)
   also have "... = setsum (\<lambda> b. setsum (count f) (?As b)) ?B" unfolding comp_def ..
   finally have "setsum (count f) ?A = setsum (\<lambda> b. setsum (count f) (?As b)) ?B" .
   thus "count (mmap (h2 \<circ> h1) f) c = count ((mmap h2 \<circ> mmap h1) f) c"
-    by transfer (unfold o_apply, blast)
+    by transfer (unfold comp_apply, blast)
 qed
 
 lemma mmap_cong:
 assumes "\<And>a. a \<in># M \<Longrightarrow> f a = g a"
 shows "mmap f M = mmap g M"

   unfolding set_of_def pcr_multiset_def cr_multiset_def fun_rel_def by auto
 
 end
 
 lemma set_of_mmap: "set_of o mmap h = image h o set_of"
-proof (rule ext, unfold o_apply)
+proof (rule ext, unfold comp_apply)
   fix M show "set_of (mmap h M) = h ` set_of M"
     by transfer (auto simp add: multiset_def setsum_gt_0_iff)
 qed
 
 lemma multiset_of_surj:

         thus ?thesis using False by auto
       next
         case True
         def c \<equiv> "f1 b1"
         have c: "c \<in> set_of P" and b1: "b1 \<in> set1 c"
-          unfolding set1_def c_def P1 using True by (auto simp: o_eq_dest[OF set_of_mmap])
+          unfolding set1_def c_def P1 using True by (auto simp: comp_eq_dest[OF set_of_mmap])
         with sM(1) have "setsum (count M) ?K = setsum (count M) {a. p1 a = b1 \<and> a \<in> SET}"
           by transfer (force intro: setsum_mono_zero_cong_left split: split_if_asm)
         also have "... = setsum (count M) ((\<lambda> b2. u c b1 b2) ` (set2 c))"
           apply(rule setsum_cong) using c b1 proof safe
           fix a assume p1a: "p1 a \<in> set1 c" and "c \<in> set_of P" and "a \<in> SET"

         thus ?thesis using False by auto
       next
         case True
         def c \<equiv> "f2 b2"
         have c: "c \<in> set_of P" and b2: "b2 \<in> set2 c"
-          unfolding set2_def c_def P2 using True by (auto simp: o_eq_dest[OF set_of_mmap])
+          unfolding set2_def c_def P2 using True by (auto simp: comp_eq_dest[OF set_of_mmap])
         with sM(1) have "setsum (count M) ?K = setsum (count M) {a. p2 a = b2 \<and> a \<in> SET}"
           by transfer (force intro: setsum_mono_zero_cong_left split: split_if_asm)
         also have "... = setsum (count M) ((\<lambda> b1. u c b1 b2) ` (set1 c))"
           apply(rule setsum_cong) using c b2 proof safe
           fix a assume p2a: "p2 a \<in> set2 c" and "c \<in> set_of P" and "a \<in> SET"

         qed auto
         also have "... = setsum (count M o (\<lambda> b1. u c b1 b2)) (set1 c)"
           apply(rule setsum_reindex)
           using inj unfolding inj_on_def inj2_def using b2 c u(2) by blast
         also have "... = setsum (\<lambda> b1. count M (u c b1 b2)) (set1 c)" by simp
-        also have "... = count N2 b2" unfolding ss2[OF c b2, symmetric] o_def
+        also have "... = count N2 b2" unfolding ss2[OF c b2, symmetric] comp_def
           apply(rule setsum_cong[OF refl]) apply (transfer fixing: Ms u c b2 set1)
           using True h_u1[OF c _ b2] u(2,3)[OF c _ b2] u_SET[OF c _ b2] set1_def by fastforce
         finally show ?thesis .
       qed
       thus "count (mmap p2 M) b2 = count N2 b2" by transfer

   from assms obtain j where j: "\<forall>a'\<in>thePull B1 B2 f1 f2.
     j a' \<in> A \<and> e1 (p1 (j a')) = e1 (fst a') \<and> e2 (p2 (j a')) = e2 (snd a')" 
     by (blast dest: wppull_thePull)
   then show ?thesis
     by (intro wpull_wppull[OF wpull_mmap[OF wpull_thePull], of _ _ _ _ "mmap j"])
-      (auto simp: o_eq_dest_lhs[OF mmap_comp[symmetric]] o_eq_dest[OF set_of_mmap]
+      (auto simp: comp_eq_dest_lhs[OF mmap_comp[symmetric]] comp_eq_dest[OF set_of_mmap]
         intro!: mmap_cong simp del: mem_set_of_iff simp: mem_set_of_iff[symmetric])
 qed
 
 bnf "'a multiset"
   map: mmap

   bd: natLeq
   wits: "{#}"
 by (auto simp add: mmap_id0 mmap_comp set_of_mmap natLeq_card_order natLeq_cinfinite set_of_bd
   Grp_def relcompp.simps intro: mmap_cong)
   (metis wppull_mmap[OF wppull_fstOp_sndOp, unfolded wppull_def
-    o_eq_dest_lhs[OF mmap_comp[symmetric]] fstOp_def sndOp_def o_def, simplified])
+    o_eq_dest_lhs[OF mmap_comp[symmetric]] fstOp_def sndOp_def comp_def, simplified])
 
 inductive rel_multiset' where
   Zero[intro]: "rel_multiset' R {#} {#}"
 | Plus[intro]: "\<lbrakk>R a b; rel_multiset' R M N\<rbrakk> \<Longrightarrow> rel_multiset' R (M + {#a#}) (N + {#b#})"