src/HOL/Library/Multiset.thy

 
 definition
   single :: "'a => 'a multiset" where
   "single a = Abs_multiset (\<lambda>b. if b = a then 1 else 0)"
 
+declare
+  Mempty_def[code func del] single_def[code func del]
+
 definition
   count :: "'a multiset => 'a => nat" where
   "count = Rep_multiset"
 
 definition

 
 instantiation multiset :: (type) "{plus, minus, zero, size}" 
 begin
 
 definition
-  union_def: "M + N == Abs_multiset (\<lambda>a. Rep_multiset M a + Rep_multiset N a)"
+  union_def[code func del]:
+  "M + N == Abs_multiset (\<lambda>a. Rep_multiset M a + Rep_multiset N a)"
 
 definition
   diff_def: "M - N == Abs_multiset (\<lambda>a. Rep_multiset M a - Rep_multiset N a)"
 
 definition
   Zero_multiset_def [simp]: "0 == {#}"
 
 definition
-  size_def: "size M == setsum (count M) (set_of M)"
+  size_def[code func del]: "size M == setsum (count M) (set_of M)"
 
 instance ..
 
 end
 

 
 text {*
  \medskip Preservation of the representing set @{term multiset}.
 *}
 
-lemma const0_in_multiset [simp]: "(\<lambda>a. 0) \<in> multiset"
+lemma const0_in_multiset: "(\<lambda>a. 0) \<in> multiset"
   by (simp add: multiset_def)
 
-lemma only1_in_multiset [simp]: "(\<lambda>b. if b = a then 1 else 0) \<in> multiset"
+lemma only1_in_multiset: "(\<lambda>b. if b = a then 1 else 0) \<in> multiset"
   by (simp add: multiset_def)
 
-lemma union_preserves_multiset [simp]:
+lemma union_preserves_multiset:
     "M \<in> multiset ==> N \<in> multiset ==> (\<lambda>a. M a + N a) \<in> multiset"
   apply (simp add: multiset_def)
   apply (drule (1) finite_UnI)
   apply (simp del: finite_Un add: Un_def)
   done
 
-lemma diff_preserves_multiset [simp]:
+lemma diff_preserves_multiset:
     "M \<in> multiset ==> (\<lambda>a. M a - N a) \<in> multiset"
   apply (simp add: multiset_def)
   apply (rule finite_subset)
    apply auto
   done
 
-
-subsection {* Algebraic properties of multisets *}
+lemma MCollect_preserves_multiset:
+    "M \<in> multiset ==> (\<lambda>x. if P x then M x else 0) \<in> multiset"
+  apply (simp add: multiset_def)
+  apply (rule finite_subset, auto)
+  done
+
+lemmas in_multiset = const0_in_multiset only1_in_multiset
+  union_preserves_multiset diff_preserves_multiset MCollect_preserves_multiset
+
+subsection {* Algebraic properties *}
 
 subsubsection {* Union *}
 
 lemma union_empty [simp]: "M + {#} = M \<and> {#} + M = M"
-  by (simp add: union_def Mempty_def)
+by (simp add: union_def Mempty_def in_multiset)
 
 lemma union_commute: "M + N = N + (M::'a multiset)"
-  by (simp add: union_def add_ac)
+by (simp add: union_def add_ac in_multiset)
 
 lemma union_assoc: "(M + N) + K = M + (N + (K::'a multiset))"
-  by (simp add: union_def add_ac)
+by (simp add: union_def add_ac in_multiset)
 
 lemma union_lcomm: "M + (N + K) = N + (M + (K::'a multiset))"
 proof -
   have "M + (N + K) = (N + K) + M"
     by (rule union_commute)

 
 
 subsubsection {* Difference *}
 
 lemma diff_empty [simp]: "M - {#} = M \<and> {#} - M = {#}"
-  by (simp add: Mempty_def diff_def)
+by (simp add: Mempty_def diff_def in_multiset)
 
 lemma diff_union_inverse2 [simp]: "M + {#a#} - {#a#} = M"
-  by (simp add: union_def diff_def)
+by (simp add: union_def diff_def in_multiset)
 
 
 subsubsection {* Count of elements *}
 
 lemma count_empty [simp]: "count {#} a = 0"
-  by (simp add: count_def Mempty_def)
+by (simp add: count_def Mempty_def in_multiset)
 
 lemma count_single [simp]: "count {#b#} a = (if b = a then 1 else 0)"
-  by (simp add: count_def single_def)
+by (simp add: count_def single_def in_multiset)
 
 lemma count_union [simp]: "count (M + N) a = count M a + count N a"
-  by (simp add: count_def union_def)
+by (simp add: count_def union_def in_multiset)
 
 lemma count_diff [simp]: "count (M - N) a = count M a - count N a"
-  by (simp add: count_def diff_def)
+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)"
+by (simp add: count_def MCollect_def in_multiset)
 
 
 subsubsection {* Set of elements *}
 
 lemma set_of_empty [simp]: "set_of {#} = {}"
-  by (simp add: set_of_def)
+by (simp add: set_of_def)
 
 lemma set_of_single [simp]: "set_of {#b#} = {b}"
-  by (simp add: set_of_def)
+by (simp add: set_of_def)
 
 lemma set_of_union [simp]: "set_of (M + N) = set_of M \<union> set_of N"
-  by (auto simp add: set_of_def)
+by (auto simp add: set_of_def)
 
 lemma set_of_eq_empty_iff [simp]: "(set_of M = {}) = (M = {#})"
-  by (auto simp add: set_of_def Mempty_def count_def expand_fun_eq)
+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)
+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}"
+by (auto simp add: set_of_def)
 
 
 subsubsection {* Size *}
 
-lemma size_empty [simp]: "size {#} = 0"
-  by (simp add: size_def)
-
-lemma size_single [simp]: "size {#b#} = 1"
-  by (simp add: size_def)
+lemma size_empty [simp,code func]: "size {#} = 0"
+by (simp add: size_def)
+
+lemma size_single [simp,code func]: "size {#b#} = 1"
+by (simp add: size_def)
 
 lemma finite_set_of [iff]: "finite (set_of M)"
   using Rep_multiset [of M]
   by (simp add: multiset_def set_of_def count_def)
 

   apply (induct rule: finite_induct)
    apply simp
   apply (simp add: Int_insert_left set_of_def)
   done
 
-lemma size_union [simp]: "size (M + N::'a multiset) = size M + size N"
+lemma size_union[simp,code func]: "size (M + N::'a multiset) = size M + size N"
   apply (unfold size_def)
   apply (subgoal_tac "count (M + N) = (\<lambda>a. count M a + count N a)")
    prefer 2
    apply (rule ext, simp)
   apply (simp (no_asm_simp) add: setsum_Un_nat setsum_addf setsum_count_Int)
   apply (subst Int_commute)
   apply (simp (no_asm_simp) add: setsum_count_Int)
   done
 
 lemma size_eq_0_iff_empty [iff]: "(size M = 0) = (M = {#})"
-  apply (unfold size_def Mempty_def count_def, auto)
-  apply (simp add: set_of_def count_def expand_fun_eq)
-  done
+apply (unfold size_def Mempty_def count_def, auto simp: in_multiset)
+apply (simp add: set_of_def count_def in_multiset expand_fun_eq)
+done
+
+lemma nonempty_has_size: "(S \<noteq> {#}) = (0 < size S)"
+by(metis gr0I gr_implies_not0 size_empty size_eq_0_iff_empty)
 
 lemma size_eq_Suc_imp_elem: "size M = Suc n ==> \<exists>a. a :# M"
   apply (unfold size_def)
   apply (drule setsum_SucD, auto)
   done

 
 lemma multiset_eq_conv_count_eq: "(M = N) = (\<forall>a. count M a = count N a)"
   by (simp add: count_def expand_fun_eq)
 
 lemma single_not_empty [simp]: "{#a#} \<noteq> {#} \<and> {#} \<noteq> {#a#}"
-  by (simp add: single_def Mempty_def expand_fun_eq)
+by (simp add: single_def Mempty_def in_multiset expand_fun_eq)
 
 lemma single_eq_single [simp]: "({#a#} = {#b#}) = (a = b)"
-  by (auto simp add: single_def expand_fun_eq)
+by (auto simp add: single_def in_multiset expand_fun_eq)
 
 lemma union_eq_empty [iff]: "(M + N = {#}) = (M = {#} \<and> N = {#})"
-  by (auto simp add: union_def Mempty_def expand_fun_eq)
+by (auto simp add: union_def Mempty_def in_multiset expand_fun_eq)
 
 lemma empty_eq_union [iff]: "({#} = M + N) = (M = {#} \<and> N = {#})"
-  by (auto simp add: union_def Mempty_def expand_fun_eq)
+by (auto simp add: union_def Mempty_def in_multiset expand_fun_eq)
 
 lemma union_right_cancel [simp]: "(M + K = N + K) = (M = (N::'a multiset))"
-  by (simp add: union_def expand_fun_eq)
+by (simp add: union_def in_multiset expand_fun_eq)
 
 lemma union_left_cancel [simp]: "(K + M = K + N) = (M = (N::'a multiset))"
-  by (simp add: union_def expand_fun_eq)
+by (simp add: union_def in_multiset expand_fun_eq)
 
 lemma union_is_single:
-    "(M + N = {#a#}) = (M = {#a#} \<and> N={#} \<or> M = {#} \<and> N = {#a#})"
-  apply (simp add: Mempty_def single_def union_def add_is_1 expand_fun_eq)
-  apply blast
-  done
+  "(M + N = {#a#}) = (M = {#a#} \<and> N={#} \<or> M = {#} \<and> N = {#a#})"
+apply (simp add: Mempty_def single_def union_def in_multiset add_is_1 expand_fun_eq)
+apply blast
+done
 
 lemma single_is_union:
      "({#a#} = M + N) = ({#a#} = M \<and> N = {#} \<or> M = {#} \<and> {#a#} = N)"
-  apply (unfold Mempty_def single_def union_def)
-  apply (simp add: add_is_1 one_is_add expand_fun_eq)
-  apply (blast dest: sym)
-  done
+apply (unfold Mempty_def single_def union_def)
+apply (simp add: add_is_1 one_is_add in_multiset expand_fun_eq)
+apply (blast dest: sym)
+done
 
 lemma add_eq_conv_diff:
   "(M + {#a#} = N + {#b#}) =
    (M = N \<and> a = b \<or> M = N - {#a#} + {#b#} \<and> N = M - {#b#} + {#a#})"
   using [[simproc del: neq]]
   apply (unfold single_def union_def diff_def)
-  apply (simp (no_asm) add: expand_fun_eq)
+  apply (simp (no_asm) add: in_multiset expand_fun_eq)
   apply (rule conjI, force, safe, simp_all)
   apply (simp add: eq_sym_conv)
   done
 
 declare Rep_multiset_inject [symmetric, simp del]

 lemma multi_union_self_other_eq: 
   "(A::'a multiset) + X = A + Y \<Longrightarrow> X = Y"
   by (induct A arbitrary: X Y, auto)
 
 lemma multi_self_add_other_not_self[simp]: "(A = A + {#x#}) = False"
-proof -
-  {
-    assume a: "A = A + {#x#}"
-    have "A = A + {#}" by simp
-    hence "A + {#} = A + {#x#}" using a by auto 
-    hence "{#} = {#x#}"
-      by - (drule multi_union_self_other_eq)
-    hence False by auto
-  }
-  thus ?thesis by blast
-qed
+by (metis single_not_empty union_empty union_left_cancel)
 
 lemma insert_noteq_member: 
   assumes BC: "B + {#b#} = C + {#c#}"
    and bnotc: "b \<noteq> c"
   shows "c \<in># B"

   hence "c \<in># B + {#b#}" using BC by simp
   thus "c \<in># B" using nc by simp
 qed
 
 
+lemma add_eq_conv_ex:
+  "(M + {#a#} = N + {#b#}) =
+    (M = N \<and> a = b \<or> (\<exists>K. M = K + {#b#} \<and> N = K + {#a#}))"
+by (auto simp add: add_eq_conv_diff)
+
+
+lemma empty_multiset_count:
+  "(\<forall>x. count A x = 0) = (A = {#})"
+by(metis count_empty multiset_eq_conv_count_eq)
+
+
 subsubsection {* Intersection *}
 
 lemma multiset_inter_count:
-    "count (A #\<inter> B) x = min (count A x) (count B x)"
-  by (simp add: multiset_inter_def min_def)
+  "count (A #\<inter> B) x = min (count A x) (count B x)"
+by (simp add: multiset_inter_def min_def)
 
 lemma multiset_inter_commute: "A #\<inter> B = B #\<inter> A"
-  by (simp add: multiset_eq_conv_count_eq multiset_inter_count
+by (simp add: multiset_eq_conv_count_eq multiset_inter_count
     min_max.inf_commute)
 
 lemma multiset_inter_assoc: "A #\<inter> (B #\<inter> C) = A #\<inter> B #\<inter> C"
-  by (simp add: multiset_eq_conv_count_eq multiset_inter_count
+by (simp add: multiset_eq_conv_count_eq multiset_inter_count
     min_max.inf_assoc)
 
 lemma multiset_inter_left_commute: "A #\<inter> (B #\<inter> C) = B #\<inter> (A #\<inter> C)"
-  by (simp add: multiset_eq_conv_count_eq multiset_inter_count min_def)
+by (simp add: multiset_eq_conv_count_eq multiset_inter_count min_def)
 
 lemmas multiset_inter_ac =
   multiset_inter_commute
   multiset_inter_assoc
   multiset_inter_left_commute

   apply (erule_tac x = a in allE)
   apply auto
   done
 
 
-subsection {* Induction over multisets *}
+subsubsection {* Comprehension (filter) *}
+
+lemma MCollect_empty[simp, code func]: "MCollect {#} P = {#}"
+by(simp add:MCollect_def Mempty_def Abs_multiset_inject in_multiset expand_fun_eq)
+
+lemma MCollect_single[simp, code func]:
+  "MCollect {#x#} P = (if P x then {#x#} else {#})"
+by(simp add:MCollect_def Mempty_def single_def Abs_multiset_inject in_multiset expand_fun_eq)
+
+lemma MCollect_union[simp, code func]:
+  "MCollect (M+N) f = MCollect M f + MCollect N f"
+by(simp add:MCollect_def union_def Abs_multiset_inject in_multiset expand_fun_eq)
+
+
+subsection {* Induction and case splits *}
 
 lemma setsum_decr:
   "finite F ==> (0::nat) < f a ==>
     setsum (f (a := f a - 1)) F = (if a\<in>F then setsum f F - 1 else setsum f F)"
   apply (induct rule: finite_induct)

     apply (subgoal_tac "f(b := f b + 1) = (\<lambda>a. f a + (if a=b then 1 else 0))")
      prefer 2
      apply (simp add: expand_fun_eq)
     apply (erule ssubst)
     apply (erule Abs_multiset_inverse [THEN subst])
-    apply (erule add [unfolded defns, simplified])
+    apply (drule add [unfolded defns, simplified])
+    apply(simp add:in_multiset)
     done
 qed
-
-lemma empty_multiset_count:
-  "(\<forall>x. count A x = 0) = (A = {#})"
-  apply (rule iffI)
-   apply (induct A, simp)
-   apply (erule_tac x=x in allE)
-   apply auto
-  done
-
-subsection {* Case splits *}
 
 lemma multi_nonempty_split: "M \<noteq> {#} \<Longrightarrow> \<exists>A a. M = A + {#a#}"
   by (induct M, auto)
 
 lemma multiset_cases [cases type, case_names empty add]:

 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 MCollect_preserves_multiset:
-    "M \<in> multiset ==> (\<lambda>x. if P x then M x else 0) \<in> multiset"
-  apply (simp add: multiset_def)
-  apply (rule finite_subset, auto)
-  done
-
-lemma count_MCollect [simp]:
-    "count {# x:M. P x #} a = (if P a then count M a else 0)"
-  by (simp add: count_def MCollect_def MCollect_preserves_multiset)
-
-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)
-
 lemma multiset_partition: "M = {# x:M. P x #} + {# x:M. \<not> P x #}"
   by (subst multiset_eq_conv_count_eq, auto)
 
-lemma add_eq_conv_ex:
-  "(M + {#a#} = N + {#b#}) =
-    (M = N \<and> a = b \<or> (\<exists>K. M = K + {#b#} \<and> N = K + {#a#}))"
-  by (auto simp add: add_eq_conv_diff)
-
 declare multiset_typedef [simp del]
-
-lemma nonempty_has_size: "(S \<noteq> {#}) = (0 < size S)"
-  apply (rule iffI)
-   apply (case_tac "size S = 0")
-    apply clarsimp
-   apply (subst (asm) neq0_conv)
-   apply auto
-  done
 
 lemma multi_drop_mem_not_eq: "c \<in># B \<Longrightarrow> B - {#c#} \<noteq> B"
   by (cases "B={#}", auto dest: multi_member_split)
 
-subsection {* Multiset orderings *}
+subsection {* Orderings *}
 
 subsubsection {* Well-foundedness *}
 
 definition
   mult1 :: "('a \<times> 'a) set => ('a multiset \<times> 'a multiset) set" where

 apply(erule union_le_mono[OF mult_le_refl])
 done
 
 subsection {* Link with lists *}
 
-consts
-  multiset_of :: "'a list \<Rightarrow> 'a multiset"
-primrec
-  "multiset_of [] = {#}"
-  "multiset_of (a # x) = multiset_of x + {# a #}"
+primrec multiset_of :: "'a list \<Rightarrow> 'a multiset" where
+"multiset_of [] = {#}" |
+"multiset_of (a # x) = multiset_of x + {# a #}"
 
 lemma multiset_of_zero_iff[simp]: "(multiset_of x = {#}) = (x = [])"
   by (induct x) auto
 
 lemma multiset_of_zero_iff_right[simp]: "({#} = multiset_of x) = (x = [])"

 lemma mset_less_diff_self: "c \<in># B \<Longrightarrow> B - {#c#} \<subset># B"
   by (auto simp: mset_le_def mset_less_def multi_drop_mem_not_eq)
 
 subsection {* Strong induction and subset induction for multisets *}
 
-subsubsection {* Well-foundedness of proper subset operator *}
+text {* Well-foundedness of proper subset operator: *}
 
 definition
   mset_less_rel  :: "('a multiset * 'a multiset) set" 
   where
   --{* proper multiset subset *}

   apply (unfold mset_less_rel_def)
   apply (rule wf_measure [THEN wf_subset, where f1=size])
   apply (clarsimp simp: measure_def inv_image_def mset_less_size)
   done
 
-subsubsection {* The induction rules *}
+text {* The induction rules: *}
 
 lemma full_multiset_induct [case_names less]:
   assumes ih: "\<And>B. \<forall>A. A \<subset># B \<longrightarrow> P A \<Longrightarrow> P B"
   shows "P B"
   apply (rule wf_mset_less_rel [THEN wf_induct])

       with P show "P F" .
     qed
   qed
 qed 
 
-subsection {* Multiset extensionality *}
+text{* A consequence: Extensionality. *}
 
 lemma multi_count_eq: 
   "(\<forall>x. count A x = count B x) = (A = B)"
   apply (rule iffI)
    prefer 2

 proof -
   from a obtain A' where "A = A' + {#a#}" by (blast dest: multi_member_split)
   thus ?thesis by simp
 qed
 
+text{* A note on code generation: When defining some
+function containing a subterm @{term"fold_mset F"}, code generation is
+not automatic. When interpreting locale @{text left_commutative} with
+@{text F}, the would be code thms for @{const fold_mset} become thms like
+@{term"fold_mset F z {#} = z"} where @{text F} is not a pattern but contains
+defined symbols, i.e.\ is not a code thm. Hence a separate constant with its
+own code thms needs to be introduced for @{text F}. See the image operator
+below. *}
+
+subsection {* Image *}
+
+definition [code func del]: "image_mset f == fold_mset (op + o single o f) {#}"
+
+interpretation image_left_comm: left_commutative["op + o single o f"]
+by(unfold_locales)(simp add:union_ac)
+
+lemma image_mset_empty[simp,code func]: "image_mset f {#} = {#}"
+by(simp add:image_mset_def)
+
+lemma image_mset_single[simp,code func]: "image_mset f {#x#} = {#f x#}"
+by(simp add:image_mset_def)
+
+lemma image_mset_insert:
+  "image_mset f (M + {#a#}) = image_mset f M + {#f a#}"
+by(simp add:image_mset_def add_ac)
+
+lemma image_mset_union[simp, code func]:
+  "image_mset f (M+N) = image_mset f M + image_mset f N"
+apply(induct N)
+ apply simp
+apply(simp add:union_assoc[symmetric] image_mset_insert)
+done
+
+lemma size_image_mset[simp]: "size(image_mset f M) = size M"
+by(induct M) simp_all
+
+lemma image_mset_is_empty_iff[simp]: "image_mset f M = {#} \<longleftrightarrow> M={#}"
+by (cases M) auto
+
+
+syntax comprehension1_mset :: "'a \<Rightarrow> 'b \<Rightarrow> 'b multiset \<Rightarrow> 'a multiset"
+       ("({#_/. _ :# _#})")
+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#}"}
+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