renamed Multiset.fold -> fold_mset, Multiset.filter -> filter_mset
authornipkow
Fri Apr 10 12:16:45 2015 +0200 (2015-04-10)
changeset 59998c54d36be22ef
parent 59994 19e5f5ac7b59
child 59999 3fa68bacfa2b
renamed Multiset.fold -> fold_mset, Multiset.filter -> filter_mset
NEWS
src/HOL/Library/DAList_Multiset.thy
src/HOL/Library/Multiset.thy
     1.1 --- a/NEWS	Thu Apr 09 23:10:08 2015 +0200
     1.2 +++ b/NEWS	Fri Apr 10 12:16:45 2015 +0200
     1.3 @@ -345,6 +345,8 @@
     1.4      INCOMPATIBILITY.
     1.5    - Renamed
     1.6        in_multiset_of ~> in_multiset_in_set
     1.7 +      Multiset.fold ~> fold_mset
     1.8 +      Multiset.filter ~> filter_mset
     1.9      INCOMPATIBILITY.
    1.10    - Removed mcard, is equal to size.
    1.11    - Added attributes:
     2.1 --- a/src/HOL/Library/DAList_Multiset.thy	Thu Apr 09 23:10:08 2015 +0200
     2.2 +++ b/src/HOL/Library/DAList_Multiset.thy	Fri Apr 10 12:16:45 2015 +0200
     2.3 @@ -24,7 +24,7 @@
     2.4  
     2.5  lemma [code, code del]: "image_mset = image_mset" ..
     2.6  
     2.7 -lemma [code, code del]: "Multiset.filter = Multiset.filter" ..
     2.8 +lemma [code, code del]: "filter_mset = filter_mset" ..
     2.9  
    2.10  lemma [code, code del]: "count = count" ..
    2.11  
    2.12 @@ -199,7 +199,7 @@
    2.13      (simp add: count_of_subtract_entries_raw alist.Alist_inverse
    2.14        distinct_subtract_entries_raw subtract_entries_def)
    2.15  
    2.16 -lemma filter_Bag [code]: "Multiset.filter P (Bag xs) = Bag (DAList.filter (P \<circ> fst) xs)"
    2.17 +lemma filter_Bag [code]: "filter_mset P (Bag xs) = Bag (DAList.filter (P \<circ> fst) xs)"
    2.18    by (rule multiset_eqI) (simp add: count_of_filter DAList.filter.rep_eq)
    2.19  
    2.20  
    2.21 @@ -285,7 +285,7 @@
    2.22  
    2.23  lemma DAList_Multiset_fold:
    2.24    assumes fn: "\<And>a n x. fn a n x = (f a ^^ n) x"
    2.25 -  shows "Multiset.fold f e (Bag al) = DAList_Multiset.fold fn e al"
    2.26 +  shows "fold_mset f e (Bag al) = DAList_Multiset.fold fn e al"
    2.27    unfolding DAList_Multiset.fold_def
    2.28  proof (induct al)
    2.29    fix ys
    2.30 @@ -294,12 +294,12 @@
    2.31    have count[simp]: "\<And>x. count (Abs_multiset (count_of x)) = count_of x"
    2.32      by (rule Abs_multiset_inverse[OF count_of_multiset])
    2.33    assume ys: "ys \<in> ?inv"
    2.34 -  then show "Multiset.fold f e (Bag (Alist ys)) = fold_impl fn e (DAList.impl_of (Alist ys))"
    2.35 +  then show "fold_mset f e (Bag (Alist ys)) = fold_impl fn e (DAList.impl_of (Alist ys))"
    2.36      unfolding Bag_def unfolding Alist_inverse[OF ys]
    2.37    proof (induct ys arbitrary: e rule: list.induct)
    2.38      case Nil
    2.39      show ?case
    2.40 -      by (rule trans[OF arg_cong[of _ "{#}" "Multiset.fold f e", OF multiset_eqI]])
    2.41 +      by (rule trans[OF arg_cong[of _ "{#}" "fold_mset f e", OF multiset_eqI]])
    2.42           (auto, simp add: cs)
    2.43    next
    2.44      case (Cons pair ys e)
    2.45 @@ -388,7 +388,7 @@
    2.46    apply (auto simp: ac_simps)
    2.47    done
    2.48  
    2.49 -lemma size_fold: "size A = Multiset.fold (\<lambda>_. Suc) 0 A" (is "_ = Multiset.fold ?f _ _")
    2.50 +lemma size_fold: "size A = fold_mset (\<lambda>_. Suc) 0 A" (is "_ = fold_mset ?f _ _")
    2.51  proof -
    2.52    interpret comp_fun_commute ?f by default auto
    2.53    show ?thesis by (induct A) auto
    2.54 @@ -403,7 +403,7 @@
    2.55  qed
    2.56  
    2.57  
    2.58 -lemma set_of_fold: "set_of A = Multiset.fold insert {} A" (is "_ = Multiset.fold ?f _ _")
    2.59 +lemma set_of_fold: "set_of A = fold_mset insert {} A" (is "_ = fold_mset ?f _ _")
    2.60  proof -
    2.61    interpret comp_fun_commute ?f by default auto
    2.62    show ?thesis by (induct A) auto
     3.1 --- a/src/HOL/Library/Multiset.thy	Thu Apr 09 23:10:08 2015 +0200
     3.2 +++ b/src/HOL/Library/Multiset.thy	Fri Apr 10 12:16:45 2015 +0200
     3.3 @@ -527,40 +527,39 @@
     3.4  
     3.5  text {* Multiset comprehension *}
     3.6  
     3.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"
     3.8 +lift_definition filter_mset :: "('a \<Rightarrow> bool) \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset"
     3.9 +is "\<lambda>P M. \<lambda>x. if P x then M x else 0"
    3.10  by (rule filter_preserves_multiset)
    3.11  
    3.12 -hide_const (open) filter
    3.13 -
    3.14 -lemma count_filter [simp]:
    3.15 -  "count (Multiset.filter P M) a = (if P a then count M a else 0)"
    3.16 -  by (simp add: filter.rep_eq)
    3.17 -
    3.18 -lemma filter_empty [simp]:
    3.19 -  "Multiset.filter P {#} = {#}"
    3.20 +lemma count_filter_mset [simp]:
    3.21 +  "count (filter_mset P M) a = (if P a then count M a else 0)"
    3.22 +  by (simp add: filter_mset.rep_eq)
    3.23 +
    3.24 +lemma filter_empty_mset [simp]:
    3.25 +  "filter_mset P {#} = {#}"
    3.26 +  by (rule multiset_eqI) simp
    3.27 +
    3.28 +lemma filter_single_mset [simp]:
    3.29 +  "filter_mset P {#x#} = (if P x then {#x#} else {#})"
    3.30    by (rule multiset_eqI) simp
    3.31  
    3.32 -lemma filter_single [simp]:
    3.33 -  "Multiset.filter P {#x#} = (if P x then {#x#} else {#})"
    3.34 +lemma filter_union_mset [simp]:
    3.35 +  "filter_mset P (M + N) = filter_mset P M + filter_mset P N"
    3.36    by (rule multiset_eqI) simp
    3.37  
    3.38 -lemma filter_union [simp]:
    3.39 -  "Multiset.filter P (M + N) = Multiset.filter P M + Multiset.filter P N"
    3.40 +lemma filter_diff_mset [simp]:
    3.41 +  "filter_mset P (M - N) = filter_mset P M - filter_mset P N"
    3.42    by (rule multiset_eqI) simp
    3.43  
    3.44 -lemma filter_diff [simp]:
    3.45 -  "Multiset.filter P (M - N) = Multiset.filter P M - Multiset.filter P N"
    3.46 +lemma filter_inter_mset [simp]:
    3.47 +  "filter_mset P (M #\<inter> N) = filter_mset P M #\<inter> filter_mset P N"
    3.48    by (rule multiset_eqI) simp
    3.49  
    3.50 -lemma filter_inter [simp]:
    3.51 -  "Multiset.filter P (M #\<inter> N) = Multiset.filter P M #\<inter> Multiset.filter P N"
    3.52 -  by (rule multiset_eqI) simp
    3.53 -
    3.54 -lemma multiset_filter_subset[simp]: "Multiset.filter f M \<le> M"
    3.55 +lemma multiset_filter_subset[simp]: "filter_mset f M \<le> M"
    3.56    unfolding less_eq_multiset.rep_eq by auto
    3.57  
    3.58  lemma multiset_filter_mono: assumes "A \<le> B"
    3.59 -  shows "Multiset.filter f A \<le> Multiset.filter f B"
    3.60 +  shows "filter_mset f A \<le> filter_mset f B"
    3.61  proof -
    3.62    from assms[unfolded mset_le_exists_conv]
    3.63    obtain C where B: "B = A + C" by auto
    3.64 @@ -572,7 +571,7 @@
    3.65  syntax (xsymbol)
    3.66    "_MCollect" :: "pttrn \<Rightarrow> 'a multiset \<Rightarrow> bool \<Rightarrow> 'a multiset"    ("(1{# _ \<in># _./ _#})")
    3.67  translations
    3.68 -  "{#x \<in># M. P#}" == "CONST Multiset.filter (\<lambda>x. P) M"
    3.69 +  "{#x \<in># M. P#}" == "CONST filter_mset (\<lambda>x. P) M"
    3.70  
    3.71  
    3.72  subsubsection {* Set of elements *}
    3.73 @@ -694,7 +693,7 @@
    3.74    show ?thesis unfolding B by (induct C, auto)
    3.75  qed
    3.76  
    3.77 -lemma size_filter_mset_lesseq[simp]: "size (Multiset.filter f M) \<le> size M"
    3.78 +lemma size_filter_mset_lesseq[simp]: "size (filter_mset f M) \<le> size M"
    3.79  by (rule size_mset_mono[OF multiset_filter_subset])
    3.80  
    3.81  lemma size_Diff_submset:
    3.82 @@ -798,19 +797,19 @@
    3.83  
    3.84  subsection {* The fold combinator *}
    3.85  
    3.86 -definition fold :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a multiset \<Rightarrow> 'b"
    3.87 +definition fold_mset :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a multiset \<Rightarrow> 'b"
    3.88  where
    3.89 -  "fold f s M = Finite_Set.fold (\<lambda>x. f x ^^ count M x) s (set_of M)"
    3.90 +  "fold_mset f s M = Finite_Set.fold (\<lambda>x. f x ^^ count M x) s (set_of M)"
    3.91  
    3.92  lemma fold_mset_empty [simp]:
    3.93 -  "fold f s {#} = s"
    3.94 -  by (simp add: fold_def)
    3.95 +  "fold_mset f s {#} = s"
    3.96 +  by (simp add: fold_mset_def)
    3.97  
    3.98  context comp_fun_commute
    3.99  begin
   3.100  
   3.101  lemma fold_mset_insert:
   3.102 -  "fold f s (M + {#x#}) = f x (fold f s M)"
   3.103 +  "fold_mset f s (M + {#x#}) = f x (fold_mset f s M)"
   3.104  proof -
   3.105    interpret mset: comp_fun_commute "\<lambda>y. f y ^^ count M y"
   3.106      by (fact comp_fun_commute_funpow)
   3.107 @@ -824,7 +823,7 @@
   3.108        Finite_Set.fold (\<lambda>y. f y ^^ count M y) s (set_of M)"
   3.109        by (auto intro!: Finite_Set.fold_cong comp_fun_commute_funpow)
   3.110      with False * show ?thesis
   3.111 -      by (simp add: fold_def del: count_union)
   3.112 +      by (simp add: fold_mset_def del: count_union)
   3.113    next
   3.114      case True
   3.115      def N \<equiv> "set_of M - {x}"
   3.116 @@ -832,23 +831,23 @@
   3.117      then have "Finite_Set.fold (\<lambda>y. f y ^^ count (M + {#x#}) y) s N =
   3.118        Finite_Set.fold (\<lambda>y. f y ^^ count M y) s N"
   3.119        by (auto intro!: Finite_Set.fold_cong comp_fun_commute_funpow)
   3.120 -    with * show ?thesis by (simp add: fold_def del: count_union) simp
   3.121 +    with * show ?thesis by (simp add: fold_mset_def del: count_union) simp
   3.122    qed
   3.123  qed
   3.124  
   3.125  corollary fold_mset_single [simp]:
   3.126 -  "fold f s {#x#} = f x s"
   3.127 +  "fold_mset f s {#x#} = f x s"
   3.128  proof -
   3.129 -  have "fold f s ({#} + {#x#}) = f x s" by (simp only: fold_mset_insert) simp
   3.130 +  have "fold_mset f s ({#} + {#x#}) = f x s" by (simp only: fold_mset_insert) simp
   3.131    then show ?thesis by simp
   3.132  qed
   3.133  
   3.134  lemma fold_mset_fun_left_comm:
   3.135 -  "f x (fold f s M) = fold f (f x s) M"
   3.136 +  "f x (fold_mset f s M) = fold_mset f (f x s) M"
   3.137    by (induct M) (simp_all add: fold_mset_insert fun_left_comm)
   3.138  
   3.139  lemma fold_mset_union [simp]:
   3.140 -  "fold f s (M + N) = fold f (fold f s M) N"
   3.141 +  "fold_mset f s (M + N) = fold_mset f (fold_mset f s M) N"
   3.142  proof (induct M)
   3.143    case empty then show ?case by simp
   3.144  next
   3.145 @@ -860,7 +859,7 @@
   3.146  
   3.147  lemma fold_mset_fusion:
   3.148    assumes "comp_fun_commute g"
   3.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")
   3.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")
   3.151  proof -
   3.152    interpret comp_fun_commute g by (fact assms)
   3.153    show "PROP ?P" by (induct A) auto
   3.154 @@ -870,10 +869,10 @@
   3.155  
   3.156  text {*
   3.157    A note on code generation: When defining some function containing a
   3.158 -  subterm @{term "fold F"}, code generation is not automatic. When
   3.159 +  subterm @{term "fold_mset F"}, code generation is not automatic. When
   3.160    interpreting locale @{text left_commutative} with @{text F}, the
   3.161 -  would be code thms for @{const fold} become thms like
   3.162 -  @{term "fold F z {#} = z"} where @{text F} is not a pattern but
   3.163 +  would be code thms for @{const fold_mset} become thms like
   3.164 +  @{term "fold_mset F z {#} = z"} where @{text F} is not a pattern but
   3.165    contains defined symbols, i.e.\ is not a code thm. Hence a separate
   3.166    constant with its own code thms needs to be introduced for @{text
   3.167    F}. See the image operator below.
   3.168 @@ -883,7 +882,7 @@
   3.169  subsection {* Image *}
   3.170  
   3.171  definition image_mset :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a multiset \<Rightarrow> 'b multiset" where
   3.172 -  "image_mset f = fold (plus o single o f) {#}"
   3.173 +  "image_mset f = fold_mset (plus o single o f) {#}"
   3.174  
   3.175  lemma comp_fun_commute_mset_image:
   3.176    "comp_fun_commute (plus o single o f)"
   3.177 @@ -1164,7 +1163,7 @@
   3.178  
   3.179  definition sorted_list_of_multiset :: "'a multiset \<Rightarrow> 'a list"
   3.180  where
   3.181 -  "sorted_list_of_multiset M = fold insort [] M"
   3.182 +  "sorted_list_of_multiset M = fold_mset insort [] M"
   3.183  
   3.184  lemma sorted_list_of_multiset_empty [simp]:
   3.185    "sorted_list_of_multiset {#} = []"
   3.186 @@ -1223,7 +1222,7 @@
   3.187  
   3.188  definition F :: "'a multiset \<Rightarrow> 'a"
   3.189  where
   3.190 -  eq_fold: "F M = Multiset.fold f 1 M"
   3.191 +  eq_fold: "F M = fold_mset f 1 M"
   3.192  
   3.193  lemma empty [simp]:
   3.194    "F {#} = 1"
   3.195 @@ -1252,7 +1251,7 @@
   3.196  
   3.197  declare comp_fun_commute.fold_mset_insert[OF comp_fun_commute_plus_mset, simp]
   3.198  
   3.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)"
   3.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)"
   3.201    by (induct NN) auto
   3.202  
   3.203  notation times (infixl "*" 70)
   3.204 @@ -1353,7 +1352,7 @@
   3.205  
   3.206  lemma msetprod_multiplicity:
   3.207    "msetprod M = setprod (\<lambda>x. x ^ count M x) (set_of M)"
   3.208 -  by (simp add: Multiset.fold_def setprod.eq_fold msetprod.eq_fold funpow_times_power comp_def)
   3.209 +  by (simp add: fold_mset_def setprod.eq_fold msetprod.eq_fold funpow_times_power comp_def)
   3.210  
   3.211  end
   3.212  
   3.213 @@ -2101,8 +2100,6 @@
   3.214      multiset_postproc
   3.215  *}
   3.216  
   3.217 -hide_const (open) fold
   3.218 -
   3.219  
   3.220  subsection {* Naive implementation using lists *}
   3.221  
   3.222 @@ -2125,7 +2122,7 @@
   3.223    by (simp add: multiset_of_map)
   3.224  
   3.225  lemma [code]:
   3.226 -  "Multiset.filter f (multiset_of xs) = multiset_of (filter f xs)"
   3.227 +  "filter_mset f (multiset_of xs) = multiset_of (filter f xs)"
   3.228    by (simp add: multiset_of_filter)
   3.229  
   3.230  lemma [code]: