src/HOL/BNF/More_BNFs.thy
changeset 55066 4e5ddf3162ac
parent 54841 af71b753c459
child 55070 235c7661a96b
     1.1 --- a/src/HOL/BNF/More_BNFs.thy	Mon Jan 20 18:24:56 2014 +0100
     1.2 +++ b/src/HOL/BNF/More_BNFs.thy	Mon Jan 20 18:24:56 2014 +0100
     1.3 @@ -17,6 +17,16 @@
     1.4    "~~/src/HOL/Library/Multiset"
     1.5  begin
     1.6  
     1.7 +notation
     1.8 +  ordLeq2 (infix "<=o" 50) and
     1.9 +  ordLeq3 (infix "\<le>o" 50) and
    1.10 +  ordLess2 (infix "<o" 50) and
    1.11 +  ordIso2 (infix "=o" 50) and
    1.12 +  csum (infixr "+c" 65) and
    1.13 +  cprod (infixr "*c" 80) and
    1.14 +  cexp (infixr "^c" 90) and
    1.15 +  convol ("<_ , _>")
    1.16 +
    1.17  lemma option_rec_conv_option_case: "option_rec = option_case"
    1.18  by (simp add: fun_eq_iff split: option.split)
    1.19  
    1.20 @@ -84,7 +94,7 @@
    1.21    thus "map f x = map g x" by simp
    1.22  next
    1.23    fix f
    1.24 -  show "set o map f = image f o set" by (rule ext, unfold o_apply, rule set_map)
    1.25 +  show "set o map f = image f o set" by (rule ext, unfold comp_apply, rule set_map)
    1.26  next
    1.27    show "card_order natLeq" by (rule natLeq_card_order)
    1.28  next
    1.29 @@ -237,7 +247,7 @@
    1.30    also have "... = setsum (\<lambda> b. setsum (count f) (?As b)) ?B" unfolding comp_def ..
    1.31    finally have "setsum (count f) ?A = setsum (\<lambda> b. setsum (count f) (?As b)) ?B" .
    1.32    thus "count (mmap (h2 \<circ> h1) f) c = count ((mmap h2 \<circ> mmap h1) f) c"
    1.33 -    by transfer (unfold o_apply, blast)
    1.34 +    by transfer (unfold comp_apply, blast)
    1.35  qed
    1.36  
    1.37  lemma mmap_cong:
    1.38 @@ -255,7 +265,7 @@
    1.39  end
    1.40  
    1.41  lemma set_of_mmap: "set_of o mmap h = image h o set_of"
    1.42 -proof (rule ext, unfold o_apply)
    1.43 +proof (rule ext, unfold comp_apply)
    1.44    fix M show "set_of (mmap h M) = h ` set_of M"
    1.45      by transfer (auto simp add: multiset_def setsum_gt_0_iff)
    1.46  qed
    1.47 @@ -687,7 +697,7 @@
    1.48          case True
    1.49          def c \<equiv> "f1 b1"
    1.50          have c: "c \<in> set_of P" and b1: "b1 \<in> set1 c"
    1.51 -          unfolding set1_def c_def P1 using True by (auto simp: o_eq_dest[OF set_of_mmap])
    1.52 +          unfolding set1_def c_def P1 using True by (auto simp: comp_eq_dest[OF set_of_mmap])
    1.53          with sM(1) have "setsum (count M) ?K = setsum (count M) {a. p1 a = b1 \<and> a \<in> SET}"
    1.54            by transfer (force intro: setsum_mono_zero_cong_left split: split_if_asm)
    1.55          also have "... = setsum (count M) ((\<lambda> b2. u c b1 b2) ` (set2 c))"
    1.56 @@ -723,7 +733,7 @@
    1.57          case True
    1.58          def c \<equiv> "f2 b2"
    1.59          have c: "c \<in> set_of P" and b2: "b2 \<in> set2 c"
    1.60 -          unfolding set2_def c_def P2 using True by (auto simp: o_eq_dest[OF set_of_mmap])
    1.61 +          unfolding set2_def c_def P2 using True by (auto simp: comp_eq_dest[OF set_of_mmap])
    1.62          with sM(1) have "setsum (count M) ?K = setsum (count M) {a. p2 a = b2 \<and> a \<in> SET}"
    1.63            by transfer (force intro: setsum_mono_zero_cong_left split: split_if_asm)
    1.64          also have "... = setsum (count M) ((\<lambda> b1. u c b1 b2) ` (set1 c))"
    1.65 @@ -738,7 +748,7 @@
    1.66            apply(rule setsum_reindex)
    1.67            using inj unfolding inj_on_def inj2_def using b2 c u(2) by blast
    1.68          also have "... = setsum (\<lambda> b1. count M (u c b1 b2)) (set1 c)" by simp
    1.69 -        also have "... = count N2 b2" unfolding ss2[OF c b2, symmetric] o_def
    1.70 +        also have "... = count N2 b2" unfolding ss2[OF c b2, symmetric] comp_def
    1.71            apply(rule setsum_cong[OF refl]) apply (transfer fixing: Ms u c b2 set1)
    1.72            using True h_u1[OF c _ b2] u(2,3)[OF c _ b2] u_SET[OF c _ b2] set1_def by fastforce
    1.73          finally show ?thesis .
    1.74 @@ -762,7 +772,7 @@
    1.75      by (blast dest: wppull_thePull)
    1.76    then show ?thesis
    1.77      by (intro wpull_wppull[OF wpull_mmap[OF wpull_thePull], of _ _ _ _ "mmap j"])
    1.78 -      (auto simp: o_eq_dest_lhs[OF mmap_comp[symmetric]] o_eq_dest[OF set_of_mmap]
    1.79 +      (auto simp: comp_eq_dest_lhs[OF mmap_comp[symmetric]] comp_eq_dest[OF set_of_mmap]
    1.80          intro!: mmap_cong simp del: mem_set_of_iff simp: mem_set_of_iff[symmetric])
    1.81  qed
    1.82  
    1.83 @@ -774,7 +784,7 @@
    1.84  by (auto simp add: mmap_id0 mmap_comp set_of_mmap natLeq_card_order natLeq_cinfinite set_of_bd
    1.85    Grp_def relcompp.simps intro: mmap_cong)
    1.86    (metis wppull_mmap[OF wppull_fstOp_sndOp, unfolded wppull_def
    1.87 -    o_eq_dest_lhs[OF mmap_comp[symmetric]] fstOp_def sndOp_def o_def, simplified])
    1.88 +    o_eq_dest_lhs[OF mmap_comp[symmetric]] fstOp_def sndOp_def comp_def, simplified])
    1.89  
    1.90  inductive rel_multiset' where
    1.91    Zero[intro]: "rel_multiset' R {#} {#}"