src/HOL/Library/Multiset.thy
changeset 59999 3fa68bacfa2b
parent 59997 90fb391a15c1
parent 59998 c54d36be22ef
child 60397 f8a513fedb31
     1.1 --- a/src/HOL/Library/Multiset.thy	Fri Apr 10 11:52:55 2015 +0200
     1.2 +++ b/src/HOL/Library/Multiset.thy	Fri Apr 10 12:16:58 2015 +0200
     1.3 @@ -527,40 +527,39 @@
     1.4  
     1.5  text {* Multiset comprehension *}
     1.6  
     1.7 -lift_definition filter :: "('a \<Rightarrow> bool) \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset" is "\<lambda>P M. \<lambda>x. if P x then M x else 0"
     1.8 +lift_definition filter_mset :: "('a \<Rightarrow> bool) \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset"
     1.9 +is "\<lambda>P M. \<lambda>x. if P x then M x else 0"
    1.10  by (rule filter_preserves_multiset)
    1.11  
    1.12 -hide_const (open) filter
    1.13 -
    1.14 -lemma count_filter [simp]:
    1.15 -  "count (Multiset.filter P M) a = (if P a then count M a else 0)"
    1.16 -  by (simp add: filter.rep_eq)
    1.17 -
    1.18 -lemma filter_empty [simp]:
    1.19 -  "Multiset.filter P {#} = {#}"
    1.20 +lemma count_filter_mset [simp]:
    1.21 +  "count (filter_mset P M) a = (if P a then count M a else 0)"
    1.22 +  by (simp add: filter_mset.rep_eq)
    1.23 +
    1.24 +lemma filter_empty_mset [simp]:
    1.25 +  "filter_mset P {#} = {#}"
    1.26 +  by (rule multiset_eqI) simp
    1.27 +
    1.28 +lemma filter_single_mset [simp]:
    1.29 +  "filter_mset P {#x#} = (if P x then {#x#} else {#})"
    1.30    by (rule multiset_eqI) simp
    1.31  
    1.32 -lemma filter_single [simp]:
    1.33 -  "Multiset.filter P {#x#} = (if P x then {#x#} else {#})"
    1.34 +lemma filter_union_mset [simp]:
    1.35 +  "filter_mset P (M + N) = filter_mset P M + filter_mset P N"
    1.36    by (rule multiset_eqI) simp
    1.37  
    1.38 -lemma filter_union [simp]:
    1.39 -  "Multiset.filter P (M + N) = Multiset.filter P M + Multiset.filter P N"
    1.40 +lemma filter_diff_mset [simp]:
    1.41 +  "filter_mset P (M - N) = filter_mset P M - filter_mset P N"
    1.42    by (rule multiset_eqI) simp
    1.43  
    1.44 -lemma filter_diff [simp]:
    1.45 -  "Multiset.filter P (M - N) = Multiset.filter P M - Multiset.filter P N"
    1.46 +lemma filter_inter_mset [simp]:
    1.47 +  "filter_mset P (M #\<inter> N) = filter_mset P M #\<inter> filter_mset P N"
    1.48    by (rule multiset_eqI) simp
    1.49  
    1.50 -lemma filter_inter [simp]:
    1.51 -  "Multiset.filter P (M #\<inter> N) = Multiset.filter P M #\<inter> Multiset.filter P N"
    1.52 -  by (rule multiset_eqI) simp
    1.53 -
    1.54 -lemma multiset_filter_subset[simp]: "Multiset.filter f M \<le> M"
    1.55 +lemma multiset_filter_subset[simp]: "filter_mset f M \<le> M"
    1.56    unfolding less_eq_multiset.rep_eq by auto
    1.57  
    1.58  lemma multiset_filter_mono: assumes "A \<le> B"
    1.59 -  shows "Multiset.filter f A \<le> Multiset.filter f B"
    1.60 +  shows "filter_mset f A \<le> filter_mset f B"
    1.61  proof -
    1.62    from assms[unfolded mset_le_exists_conv]
    1.63    obtain C where B: "B = A + C" by auto
    1.64 @@ -572,7 +571,7 @@
    1.65  syntax (xsymbol)
    1.66    "_MCollect" :: "pttrn \<Rightarrow> 'a multiset \<Rightarrow> bool \<Rightarrow> 'a multiset"    ("(1{# _ \<in># _./ _#})")
    1.67  translations
    1.68 -  "{#x \<in># M. P#}" == "CONST Multiset.filter (\<lambda>x. P) M"
    1.69 +  "{#x \<in># M. P#}" == "CONST filter_mset (\<lambda>x. P) M"
    1.70  
    1.71  
    1.72  subsubsection {* Set of elements *}
    1.73 @@ -694,7 +693,7 @@
    1.74    show ?thesis unfolding B by (induct C, auto)
    1.75  qed
    1.76  
    1.77 -lemma size_filter_mset_lesseq[simp]: "size (Multiset.filter f M) \<le> size M"
    1.78 +lemma size_filter_mset_lesseq[simp]: "size (filter_mset f M) \<le> size M"
    1.79  by (rule size_mset_mono[OF multiset_filter_subset])
    1.80  
    1.81  lemma size_Diff_submset:
    1.82 @@ -798,19 +797,19 @@
    1.83  
    1.84  subsection {* The fold combinator *}
    1.85  
    1.86 -definition fold :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a multiset \<Rightarrow> 'b"
    1.87 +definition fold_mset :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a multiset \<Rightarrow> 'b"
    1.88  where
    1.89 -  "fold f s M = Finite_Set.fold (\<lambda>x. f x ^^ count M x) s (set_of M)"
    1.90 +  "fold_mset f s M = Finite_Set.fold (\<lambda>x. f x ^^ count M x) s (set_of M)"
    1.91  
    1.92  lemma fold_mset_empty [simp]:
    1.93 -  "fold f s {#} = s"
    1.94 -  by (simp add: fold_def)
    1.95 +  "fold_mset f s {#} = s"
    1.96 +  by (simp add: fold_mset_def)
    1.97  
    1.98  context comp_fun_commute
    1.99  begin
   1.100  
   1.101  lemma fold_mset_insert:
   1.102 -  "fold f s (M + {#x#}) = f x (fold f s M)"
   1.103 +  "fold_mset f s (M + {#x#}) = f x (fold_mset f s M)"
   1.104  proof -
   1.105    interpret mset: comp_fun_commute "\<lambda>y. f y ^^ count M y"
   1.106      by (fact comp_fun_commute_funpow)
   1.107 @@ -824,7 +823,7 @@
   1.108        Finite_Set.fold (\<lambda>y. f y ^^ count M y) s (set_of M)"
   1.109        by (auto intro!: Finite_Set.fold_cong comp_fun_commute_funpow)
   1.110      with False * show ?thesis
   1.111 -      by (simp add: fold_def del: count_union)
   1.112 +      by (simp add: fold_mset_def del: count_union)
   1.113    next
   1.114      case True
   1.115      def N \<equiv> "set_of M - {x}"
   1.116 @@ -832,23 +831,23 @@
   1.117      then have "Finite_Set.fold (\<lambda>y. f y ^^ count (M + {#x#}) y) s N =
   1.118        Finite_Set.fold (\<lambda>y. f y ^^ count M y) s N"
   1.119        by (auto intro!: Finite_Set.fold_cong comp_fun_commute_funpow)
   1.120 -    with * show ?thesis by (simp add: fold_def del: count_union) simp
   1.121 +    with * show ?thesis by (simp add: fold_mset_def del: count_union) simp
   1.122    qed
   1.123  qed
   1.124  
   1.125  corollary fold_mset_single [simp]:
   1.126 -  "fold f s {#x#} = f x s"
   1.127 +  "fold_mset f s {#x#} = f x s"
   1.128  proof -
   1.129 -  have "fold f s ({#} + {#x#}) = f x s" by (simp only: fold_mset_insert) simp
   1.130 +  have "fold_mset f s ({#} + {#x#}) = f x s" by (simp only: fold_mset_insert) simp
   1.131    then show ?thesis by simp
   1.132  qed
   1.133  
   1.134  lemma fold_mset_fun_left_comm:
   1.135 -  "f x (fold f s M) = fold f (f x s) M"
   1.136 +  "f x (fold_mset f s M) = fold_mset f (f x s) M"
   1.137    by (induct M) (simp_all add: fold_mset_insert fun_left_comm)
   1.138  
   1.139  lemma fold_mset_union [simp]:
   1.140 -  "fold f s (M + N) = fold f (fold f s M) N"
   1.141 +  "fold_mset f s (M + N) = fold_mset f (fold_mset f s M) N"
   1.142  proof (induct M)
   1.143    case empty then show ?case by simp
   1.144  next
   1.145 @@ -860,7 +859,7 @@
   1.146  
   1.147  lemma fold_mset_fusion:
   1.148    assumes "comp_fun_commute g"
   1.149 -  shows "(\<And>x y. h (g x y) = f x (h y)) \<Longrightarrow> h (fold g w A) = fold f (h w) A" (is "PROP ?P")
   1.150 +  shows "(\<And>x y. h (g x y) = f x (h y)) \<Longrightarrow> h (fold_mset g w A) = fold_mset f (h w) A" (is "PROP ?P")
   1.151  proof -
   1.152    interpret comp_fun_commute g by (fact assms)
   1.153    show "PROP ?P" by (induct A) auto
   1.154 @@ -870,10 +869,10 @@
   1.155  
   1.156  text {*
   1.157    A note on code generation: When defining some function containing a
   1.158 -  subterm @{term "fold F"}, code generation is not automatic. When
   1.159 +  subterm @{term "fold_mset F"}, code generation is not automatic. When
   1.160    interpreting locale @{text left_commutative} with @{text F}, the
   1.161 -  would be code thms for @{const fold} become thms like
   1.162 -  @{term "fold F z {#} = z"} where @{text F} is not a pattern but
   1.163 +  would be code thms for @{const fold_mset} become thms like
   1.164 +  @{term "fold_mset F z {#} = z"} where @{text F} is not a pattern but
   1.165    contains defined symbols, i.e.\ is not a code thm. Hence a separate
   1.166    constant with its own code thms needs to be introduced for @{text
   1.167    F}. See the image operator below.
   1.168 @@ -883,7 +882,7 @@
   1.169  subsection {* Image *}
   1.170  
   1.171  definition image_mset :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a multiset \<Rightarrow> 'b multiset" where
   1.172 -  "image_mset f = fold (plus o single o f) {#}"
   1.173 +  "image_mset f = fold_mset (plus o single o f) {#}"
   1.174  
   1.175  lemma comp_fun_commute_mset_image:
   1.176    "comp_fun_commute (plus o single o f)"
   1.177 @@ -1164,7 +1163,7 @@
   1.178  
   1.179  definition sorted_list_of_multiset :: "'a multiset \<Rightarrow> 'a list"
   1.180  where
   1.181 -  "sorted_list_of_multiset M = fold insort [] M"
   1.182 +  "sorted_list_of_multiset M = fold_mset insort [] M"
   1.183  
   1.184  lemma sorted_list_of_multiset_empty [simp]:
   1.185    "sorted_list_of_multiset {#} = []"
   1.186 @@ -1223,7 +1222,7 @@
   1.187  
   1.188  definition F :: "'a multiset \<Rightarrow> 'a"
   1.189  where
   1.190 -  eq_fold: "F M = Multiset.fold f 1 M"
   1.191 +  eq_fold: "F M = fold_mset f 1 M"
   1.192  
   1.193  lemma empty [simp]:
   1.194    "F {#} = 1"
   1.195 @@ -1252,7 +1251,7 @@
   1.196  
   1.197  declare comp_fun_commute.fold_mset_insert[OF comp_fun_commute_plus_mset, simp]
   1.198  
   1.199 -lemma in_mset_fold_plus_iff[iff]: "x \<in># Multiset.fold (op +) M NN \<longleftrightarrow> x \<in># M \<or> (\<exists>N. N \<in># NN \<and> x \<in># N)"
   1.200 +lemma in_mset_fold_plus_iff[iff]: "x \<in># fold_mset (op +) M NN \<longleftrightarrow> x \<in># M \<or> (\<exists>N. N \<in># NN \<and> x \<in># N)"
   1.201    by (induct NN) auto
   1.202  
   1.203  notation times (infixl "*" 70)
   1.204 @@ -1353,7 +1352,7 @@
   1.205  
   1.206  lemma msetprod_multiplicity:
   1.207    "msetprod M = setprod (\<lambda>x. x ^ count M x) (set_of M)"
   1.208 -  by (simp add: Multiset.fold_def setprod.eq_fold msetprod.eq_fold funpow_times_power comp_def)
   1.209 +  by (simp add: fold_mset_def setprod.eq_fold msetprod.eq_fold funpow_times_power comp_def)
   1.210  
   1.211  end
   1.212  
   1.213 @@ -2101,8 +2100,6 @@
   1.214      multiset_postproc
   1.215  *}
   1.216  
   1.217 -hide_const (open) fold
   1.218 -
   1.219  
   1.220  subsection {* Naive implementation using lists *}
   1.221  
   1.222 @@ -2125,7 +2122,7 @@
   1.223    by (simp add: multiset_of_map)
   1.224  
   1.225  lemma [code]:
   1.226 -  "Multiset.filter f (multiset_of xs) = multiset_of (filter f xs)"
   1.227 +  "filter_mset f (multiset_of xs) = multiset_of (filter f xs)"
   1.228    by (simp add: multiset_of_filter)
   1.229  
   1.230  lemma [code]: