src/HOL/Library/Multiset.thy

   "a :# M == 0 < count M a"
 
 notation (xsymbols) Melem (infix "\<in>#" 50)
 
 syntax
-  "_MCollect" :: "pttrn => 'a multiset => bool => 'a multiset"    ("(1{# _ : _./ _#})")
+  "_MCollect" :: "pttrn => 'a multiset => bool => 'a multiset"    ("(1{# _ :# _./ _#})")
 translations
-  "{#x:M. P#}" == "CONST MCollect M (\<lambda>x. P)"
+  "{#x :# M. P#}" == "CONST MCollect M (\<lambda>x. P)"
 
 definition
   set_of :: "'a multiset => 'a set" where
   "set_of M = {x. x :# M}"
 

 
 lemma count_diff [simp]: "count (M - N) a = count M a - count N a"
 by (simp add: count_def diff_def in_multiset)
 
 lemma count_MCollect [simp]:
-  "count {# x:M. P x #} a = (if P a then count M a else 0)"
+  "count {# x:#M. P x #} a = (if P a then count M a else 0)"
 by (simp add: count_def MCollect_def in_multiset)
 
 
 subsubsection {* Set of elements *}
 

 by(auto simp: set_of_def Mempty_def in_multiset count_def expand_fun_eq)
 
 lemma mem_set_of_iff [simp]: "(x \<in> set_of M) = (x :# M)"
 by (auto simp add: set_of_def)
 
-lemma set_of_MCollect [simp]: "set_of {# x:M. P x #} = set_of M \<inter> {x. P x}"
+lemma set_of_MCollect [simp]: "set_of {# x:#M. P x #} = set_of M \<inter> {x. P x}"
 by (auto simp add: set_of_def)
 
 
 subsubsection {* Size *}
 

 lemma multi_member_split: "x \<in># M \<Longrightarrow> \<exists>A. M = A + {#x#}"
   apply (cases M, simp)
   apply (rule_tac x="M - {#x#}" in exI, simp)
   done
 
-lemma multiset_partition: "M = {# x:M. P x #} + {# x:M. \<not> P x #}"
+lemma multiset_partition: "M = {# x:#M. P x #} + {# x:#M. \<not> P x #}"
   by (subst multiset_eq_conv_count_eq, auto)
 
 declare multiset_typedef [simp del]
 
 lemma multi_drop_mem_not_eq: "c \<in># B \<Longrightarrow> B - {#c#} \<noteq> B"

   apply (cut_tac M = K and P = "\<lambda>x. (x, a) \<in> r" in multiset_partition)
   apply (erule_tac P = "\<forall>k \<in> set_of K. ?P k" in rev_mp)
   apply (erule ssubst)
   apply (simp add: Ball_def, auto)
   apply (subgoal_tac
-    "((I + {# x : K. (x, a) \<in> r #}) + {# x : K. (x, a) \<notin> r #},
-      (I + {# x : K. (x, a) \<in> r #}) + J') \<in> mult r")
+    "((I + {# x :# K. (x, a) \<in> r #}) + {# x :# K. (x, a) \<notin> r #},
+      (I + {# x :# K. (x, a) \<in> r #}) + J') \<in> mult r")
    prefer 2
    apply force
   apply (simp (no_asm_use) add: union_assoc [symmetric] mult_def)
   apply (erule trancl_trans)
   apply (rule r_into_trancl)

 translations "{#e. x:#M#}" == "CONST image_mset (%x. e) M"
 
 syntax comprehension2_mset :: "'a \<Rightarrow> 'b \<Rightarrow> 'b multiset \<Rightarrow> bool \<Rightarrow> 'a multiset"
        ("({#_/ | _ :# _./ _#})")
 translations
-  "{#e | x:#M. P#}" => "{#e. x :# {# x:M. P#}#}"
-
-text{* This allows to write not just filters like @{term"{#x:M. x<c#}"}
+  "{#e | x:#M. P#}" => "{#e. x :# {# x:#M. P#}#}"
+
+text{* This allows to write not just filters like @{term"{#x:#M. x<c#}"}
 but also images like @{term"{#x+x. x:#M #}"}
 and @{term[source]"{#x+x|x:#M. x<c#}"}, where the latter is currently
 displayed as @{term"{#x+x|x:#M. x<c#}"}. *}
 
 end