--- a/NEWS Thu Jun 18 16:17:51 2015 +0200
+++ b/NEWS Fri Jun 19 15:55:22 2015 +0200
@@ -116,8 +116,9 @@
(e.g. add_mono ~> subset_mset.add_mono).
INCOMPATIBILITY.
- Renamed conversions:
+ multiset_of ~> mset
+ multiset_of_set ~> mset_set
set_of ~> set_mset
- multiset_of_set ~> mset_set
INCOMPATIBILITY
- Renamed lemmas:
mset_le_def ~> subseteq_mset_def
--- a/src/HOL/Algebra/Divisibility.thy Thu Jun 18 16:17:51 2015 +0200
+++ b/src/HOL/Algebra/Divisibility.thy Fri Jun 19 15:55:22 2015 +0200
@@ -1063,9 +1063,9 @@
shows "P (set bs)"
proof -
from perm
- have "multiset_of as = multiset_of bs"
- by (simp add: multiset_of_eq_perm)
- hence "set as = set bs" by (rule multiset_of_eq_setD)
+ have "mset as = mset bs"
+ by (simp add: mset_eq_perm)
+ hence "set as = set bs" by (rule mset_eq_setD)
with as
show "P (set bs)" by simp
qed
@@ -1792,7 +1792,7 @@
"assocs G x == eq_closure_of (division_rel G) {x}"
definition
- "fmset G as = multiset_of (map (\<lambda>a. assocs G a) as)"
+ "fmset G as = mset (map (\<lambda>a. assocs G a) as)"
text {* Helper lemmas *}
@@ -1840,7 +1840,7 @@
assumes prm: "as <~~> bs"
shows "fmset G as = fmset G bs"
using perm_map[OF prm]
-by (simp add: multiset_of_eq_perm fmset_def)
+by (simp add: mset_eq_perm fmset_def)
lemma (in comm_monoid_cancel) eqc_listassoc_cong:
assumes "as [\<sim>] bs"
@@ -1923,9 +1923,9 @@
and p3: "map (assocs G) as <~~> map (assocs G) bs"
from p1
- have "multiset_of (map (assocs G) as) = multiset_of ys"
- by (simp add: multiset_of_eq_perm)
- hence setys: "set (map (assocs G) as) = set ys" by (rule multiset_of_eq_setD)
+ have "mset (map (assocs G) as) = mset ys"
+ by (simp add: mset_eq_perm)
+ hence setys: "set (map (assocs G) as) = set ys" by (rule mset_eq_setD)
have "set (map (assocs G) as) = { assocs G x | x. x \<in> set as}" by clarsimp fast
with setys have "set ys \<subseteq> { assocs G x | x. x \<in> set as}" by simp
@@ -1980,7 +1980,7 @@
proof -
from mset
have mpp: "map (assocs G) as <~~> map (assocs G) bs"
- by (simp add: fmset_def multiset_of_eq_perm)
+ by (simp add: fmset_def mset_eq_perm)
have "\<exists>cas. cas = map (assocs G) as" by simp
from this obtain cas where cas: "cas = map (assocs G) as" by simp
@@ -2003,7 +2003,7 @@
and tm: "map (assocs G) as' = map (assocs G) bs"
by auto
from tm have lene: "length as' = length bs" by (rule map_eq_imp_length_eq)
- from tp have "set as = set as'" by (simp add: multiset_of_eq_perm multiset_of_eq_setD)
+ from tp have "set as = set as'" by (simp add: mset_eq_perm mset_eq_setD)
with ascarr
have as'carr: "set as' \<subseteq> carrier G" by simp
@@ -2028,13 +2028,13 @@
assumes elems: "\<And>X. X \<in> set_mset Cs \<Longrightarrow> \<exists>x. P x \<and> X = assocs G x"
shows "\<exists>cs. (\<forall>c \<in> set cs. P c) \<and> fmset G cs = Cs"
proof -
- have "\<exists>Cs'. Cs = multiset_of Cs'"
- by (rule surjE[OF surj_multiset_of], fast)
+ have "\<exists>Cs'. Cs = mset Cs'"
+ by (rule surjE[OF surj_mset], fast)
from this obtain Cs'
- where Cs: "Cs = multiset_of Cs'"
+ where Cs: "Cs = mset Cs'"
by auto
- have "\<exists>cs. (\<forall>c \<in> set cs. P c) \<and> multiset_of (map (assocs G) cs) = Cs"
+ have "\<exists>cs. (\<forall>c \<in> set cs. P c) \<and> mset (map (assocs G) cs) = Cs"
using elems
unfolding Cs
apply (induct Cs', simp)
@@ -2042,7 +2042,7 @@
fix a Cs' cs
assume ih: "\<And>X. X = a \<or> X \<in> set Cs' \<Longrightarrow> \<exists>x. P x \<and> X = assocs G x"
and csP: "\<forall>x\<in>set cs. P x"
- and mset: "multiset_of (map (assocs G) cs) = multiset_of Cs'"
+ and mset: "mset (map (assocs G) cs) = mset Cs'"
from ih
have "\<exists>x. P x \<and> a = assocs G x" by fast
from this obtain c
@@ -2052,11 +2052,11 @@
from cP csP
have tP: "\<forall>x\<in>set (c#cs). P x" by simp
from mset a
- have "multiset_of (map (assocs G) (c#cs)) = multiset_of Cs' + {#a#}" by simp
+ have "mset (map (assocs G) (c#cs)) = mset Cs' + {#a#}" by simp
from tP this
show "\<exists>cs. (\<forall>x\<in>set cs. P x) \<and>
- multiset_of (map (assocs G) cs) =
- multiset_of Cs' + {#a#}" by fast
+ mset (map (assocs G) cs) =
+ mset Cs' + {#a#}" by fast
qed
thus ?thesis by (simp add: fmset_def)
qed
--- a/src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy Thu Jun 18 16:17:51 2015 +0200
+++ b/src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy Fri Jun 19 15:55:22 2015 +0200
@@ -34,11 +34,11 @@
lemma swap_permutes:
assumes "effect (swap a i j) h h' rs"
- shows "multiset_of (Array.get h' a)
- = multiset_of (Array.get h a)"
+ shows "mset (Array.get h' a)
+ = mset (Array.get h a)"
using assms
unfolding swap_def
- by (auto simp add: Array.length_def multiset_of_swap dest: sym [of _ "h'"] elim!: effect_bindE effect_nthE effect_returnE effect_updE)
+ by (auto simp add: Array.length_def mset_swap dest: sym [of _ "h'"] elim!: effect_bindE effect_nthE effect_returnE effect_updE)
function part1 :: "nat array \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat Heap"
where
@@ -59,8 +59,8 @@
lemma part_permutes:
assumes "effect (part1 a l r p) h h' rs"
- shows "multiset_of (Array.get h' a)
- = multiset_of (Array.get h a)"
+ shows "mset (Array.get h' a)
+ = mset (Array.get h a)"
using assms
proof (induct a l r p arbitrary: h h' rs rule:part1.induct)
case (1 a l r p h h' rs)
@@ -244,8 +244,8 @@
lemma partition_permutes:
assumes "effect (partition a l r) h h' rs"
- shows "multiset_of (Array.get h' a)
- = multiset_of (Array.get h a)"
+ shows "mset (Array.get h' a)
+ = mset (Array.get h a)"
proof -
from assms part_permutes swap_permutes show ?thesis
unfolding partition.simps
@@ -424,8 +424,8 @@
lemma quicksort_permutes:
assumes "effect (quicksort a l r) h h' rs"
- shows "multiset_of (Array.get h' a)
- = multiset_of (Array.get h a)"
+ shows "mset (Array.get h' a)
+ = mset (Array.get h a)"
using assms
proof (induct a l r arbitrary: h h' rs rule: quicksort.induct)
case (1 a l r h h' rs)
@@ -533,23 +533,23 @@
and part_conds2: "\<forall>j. j \<in> set (subarray (p + 1) (r + 1) a h1) \<longrightarrow> Array.get h1 a ! p \<le> j"
by (auto simp add: all_in_set_subarray_conv)
from quicksort_outer_remains [OF qs1] quicksort_permutes [OF qs1] True
- length_remains 1(5) pivot multiset_of_sublist [of l p "Array.get h1 a" "Array.get h2 a"]
- have multiset_partconds1: "multiset_of (subarray l p a h2) = multiset_of (subarray l p a h1)"
+ length_remains 1(5) pivot mset_sublist [of l p "Array.get h1 a" "Array.get h2 a"]
+ have multiset_partconds1: "mset (subarray l p a h2) = mset (subarray l p a h1)"
unfolding Array.length_def subarray_def by (cases p, auto)
with left_subarray_remains part_conds1 pivot_unchanged
have part_conds2': "\<forall>j. j \<in> set (subarray l p a h') \<longrightarrow> j \<le> Array.get h' a ! p"
- by (simp, subst set_mset_multiset_of[symmetric], simp)
+ by (simp, subst set_mset_mset[symmetric], simp)
(* -- These steps are the analogous for the right sublist \<dots> *)
from quicksort_outer_remains [OF qs1] length_remains
have right_subarray_remains: "subarray (p + 1) (r + 1) a h1 = subarray (p + 1) (r + 1) a h2"
by (auto simp add: subarray_eq_samelength_iff)
from quicksort_outer_remains [OF qs2] quicksort_permutes [OF qs2] True
- length_remains 1(5) pivot multiset_of_sublist [of "p + 1" "r + 1" "Array.get h2 a" "Array.get h' a"]
- have multiset_partconds2: "multiset_of (subarray (p + 1) (r + 1) a h') = multiset_of (subarray (p + 1) (r + 1) a h2)"
+ length_remains 1(5) pivot mset_sublist [of "p + 1" "r + 1" "Array.get h2 a" "Array.get h' a"]
+ have multiset_partconds2: "mset (subarray (p + 1) (r + 1) a h') = mset (subarray (p + 1) (r + 1) a h2)"
unfolding Array.length_def subarray_def by auto
with right_subarray_remains part_conds2 pivot_unchanged
have part_conds1': "\<forall>j. j \<in> set (subarray (p + 1) (r + 1) a h') \<longrightarrow> Array.get h' a ! p \<le> j"
- by (simp, subst set_mset_multiset_of[symmetric], simp)
+ by (simp, subst set_mset_mset[symmetric], simp)
(* -- Thirdly and finally, we show that the array is sorted
following from the facts above. *)
from True pivot 1(5) length_remains have "subarray l (r + 1) a h' = subarray l p a h' @ [Array.get h' a ! p] @ subarray (p + 1) (r + 1) a h'"
--- a/src/HOL/Imperative_HOL/ex/Sublist.thy Thu Jun 18 16:17:51 2015 +0200
+++ b/src/HOL/Imperative_HOL/ex/Sublist.thy Fri Jun 19 15:55:22 2015 +0200
@@ -471,26 +471,26 @@
unfolding set_sublist' by blast
-lemma multiset_of_sublist:
+lemma mset_sublist:
assumes l_r: "l \<le> r \<and> r \<le> List.length xs"
assumes left: "\<forall> i. i < l \<longrightarrow> (xs::'a list) ! i = ys ! i"
assumes right: "\<forall> i. i \<ge> r \<longrightarrow> (xs::'a list) ! i = ys ! i"
-assumes multiset: "multiset_of xs = multiset_of ys"
- shows "multiset_of (sublist' l r xs) = multiset_of (sublist' l r ys)"
+assumes multiset: "mset xs = mset ys"
+ shows "mset (sublist' l r xs) = mset (sublist' l r ys)"
proof -
from l_r have xs_def: "xs = (sublist' 0 l xs) @ (sublist' l r xs) @ (sublist' r (List.length xs) xs)" (is "_ = ?xs_long")
by (simp add: sublist'_append)
- from multiset have length_eq: "List.length xs = List.length ys" by (rule multiset_of_eq_length)
+ from multiset have length_eq: "List.length xs = List.length ys" by (rule mset_eq_length)
with l_r have ys_def: "ys = (sublist' 0 l ys) @ (sublist' l r ys) @ (sublist' r (List.length ys) ys)" (is "_ = ?ys_long")
by (simp add: sublist'_append)
- from xs_def ys_def multiset have "multiset_of ?xs_long = multiset_of ?ys_long" by simp
+ from xs_def ys_def multiset have "mset ?xs_long = mset ?ys_long" by simp
moreover
from left l_r length_eq have "sublist' 0 l xs = sublist' 0 l ys"
by (auto simp add: length_sublist' nth_sublist' intro!: nth_equalityI)
moreover
from right l_r length_eq have "sublist' r (List.length xs) xs = sublist' r (List.length ys) ys"
by (auto simp add: length_sublist' nth_sublist' intro!: nth_equalityI)
- ultimately show ?thesis by (simp add: multiset_of_append)
+ ultimately show ?thesis by (simp add: mset_append)
qed
--- a/src/HOL/Library/DAList_Multiset.thy Thu Jun 18 16:17:51 2015 +0200
+++ b/src/HOL/Library/DAList_Multiset.thy Fri Jun 19 15:55:22 2015 +0200
@@ -267,7 +267,7 @@
declare multiset_inter_def [code]
declare sup_subset_mset_def [code]
-declare multiset_of.simps [code]
+declare mset.simps [code]
fun fold_impl :: "('a \<Rightarrow> nat \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> ('a \<times> nat) list \<Rightarrow> 'b"
--- a/src/HOL/Library/Multiset.thy Thu Jun 18 16:17:51 2015 +0200
+++ b/src/HOL/Library/Multiset.thy Fri Jun 19 15:55:22 2015 +0200
@@ -963,46 +963,46 @@
subsection \<open>Further conversions\<close>
-primrec multiset_of :: "'a list \<Rightarrow> 'a multiset" where
- "multiset_of [] = {#}" |
- "multiset_of (a # x) = multiset_of x + {# a #}"
+primrec mset :: "'a list \<Rightarrow> 'a multiset" where
+ "mset [] = {#}" |
+ "mset (a # x) = mset x + {# a #}"
lemma in_multiset_in_set:
- "x \<in># multiset_of xs \<longleftrightarrow> x \<in> set xs"
+ "x \<in># mset xs \<longleftrightarrow> x \<in> set xs"
by (induct xs) simp_all
-lemma count_multiset_of:
- "count (multiset_of xs) x = length (filter (\<lambda>y. x = y) xs)"
+lemma count_mset:
+ "count (mset xs) x = length (filter (\<lambda>y. x = y) xs)"
by (induct xs) simp_all
-lemma multiset_of_zero_iff[simp]: "(multiset_of x = {#}) = (x = [])"
+lemma mset_zero_iff[simp]: "(mset x = {#}) = (x = [])"
by (induct x) auto
-lemma multiset_of_zero_iff_right[simp]: "({#} = multiset_of x) = (x = [])"
+lemma mset_zero_iff_right[simp]: "({#} = mset x) = (x = [])"
by (induct x) auto
-lemma set_mset_multiset_of[simp]: "set_mset (multiset_of x) = set x"
+lemma set_mset_mset[simp]: "set_mset (mset x) = set x"
by (induct x) auto
-lemma mem_set_multiset_eq: "x \<in> set xs = (x :# multiset_of xs)"
+lemma mem_set_multiset_eq: "x \<in> set xs = (x :# mset xs)"
by (induct xs) auto
-lemma size_multiset_of [simp]: "size (multiset_of xs) = length xs"
+lemma size_mset [simp]: "size (mset xs) = length xs"
by (induct xs) simp_all
-lemma multiset_of_append [simp]:
- "multiset_of (xs @ ys) = multiset_of xs + multiset_of ys"
+lemma mset_append [simp]:
+ "mset (xs @ ys) = mset xs + mset ys"
by (induct xs arbitrary: ys) (auto simp: ac_simps)
-lemma multiset_of_filter:
- "multiset_of (filter P xs) = {#x :# multiset_of xs. P x #}"
+lemma mset_filter:
+ "mset (filter P xs) = {#x :# mset xs. P x #}"
by (induct xs) simp_all
-lemma multiset_of_rev [simp]:
- "multiset_of (rev xs) = multiset_of xs"
+lemma mset_rev [simp]:
+ "mset (rev xs) = mset xs"
by (induct xs) simp_all
-lemma surj_multiset_of: "surj multiset_of"
+lemma surj_mset: "surj mset"
apply (unfold surj_def)
apply (rule allI)
apply (rule_tac M = y in multiset_induct)
@@ -1011,72 +1011,72 @@
apply auto
done
-lemma set_count_greater_0: "set x = {a. count (multiset_of x) a > 0}"
+lemma set_count_greater_0: "set x = {a. count (mset x) a > 0}"
by (induct x) auto
lemma distinct_count_atmost_1:
- "distinct x = (! a. count (multiset_of x) a = (if a \<in> set x then 1 else 0))"
+ "distinct x = (! a. count (mset x) a = (if a \<in> set x then 1 else 0))"
apply (induct x, simp, rule iffI, simp_all)
apply (rename_tac a b)
apply (rule conjI)
-apply (simp_all add: set_mset_multiset_of [THEN sym] del: set_mset_multiset_of)
+apply (simp_all add: set_mset_mset [THEN sym] del: set_mset_mset)
apply (erule_tac x = a in allE, simp, clarify)
apply (erule_tac x = aa in allE, simp)
done
-lemma multiset_of_eq_setD:
- "multiset_of xs = multiset_of ys \<Longrightarrow> set xs = set ys"
+lemma mset_eq_setD:
+ "mset xs = mset ys \<Longrightarrow> set xs = set ys"
by (rule) (auto simp add:multiset_eq_iff set_count_greater_0)
-lemma set_eq_iff_multiset_of_eq_distinct:
+lemma set_eq_iff_mset_eq_distinct:
"distinct x \<Longrightarrow> distinct y \<Longrightarrow>
- (set x = set y) = (multiset_of x = multiset_of y)"
+ (set x = set y) = (mset x = mset y)"
by (auto simp: multiset_eq_iff distinct_count_atmost_1)
-lemma set_eq_iff_multiset_of_remdups_eq:
- "(set x = set y) = (multiset_of (remdups x) = multiset_of (remdups y))"
+lemma set_eq_iff_mset_remdups_eq:
+ "(set x = set y) = (mset (remdups x) = mset (remdups y))"
apply (rule iffI)
-apply (simp add: set_eq_iff_multiset_of_eq_distinct[THEN iffD1])
+apply (simp add: set_eq_iff_mset_eq_distinct[THEN iffD1])
apply (drule distinct_remdups [THEN distinct_remdups
- [THEN set_eq_iff_multiset_of_eq_distinct [THEN iffD2]]])
+ [THEN set_eq_iff_mset_eq_distinct [THEN iffD2]]])
apply simp
done
-lemma multiset_of_compl_union [simp]:
- "multiset_of [x\<leftarrow>xs. P x] + multiset_of [x\<leftarrow>xs. \<not>P x] = multiset_of xs"
+lemma mset_compl_union [simp]:
+ "mset [x\<leftarrow>xs. P x] + mset [x\<leftarrow>xs. \<not>P x] = mset xs"
by (induct xs) (auto simp: ac_simps)
-lemma nth_mem_multiset_of: "i < length ls \<Longrightarrow> (ls ! i) :# multiset_of ls"
+lemma nth_mem_mset: "i < length ls \<Longrightarrow> (ls ! i) :# mset ls"
apply (induct ls arbitrary: i)
apply simp
apply (case_tac i)
apply auto
done
-lemma multiset_of_remove1[simp]:
- "multiset_of (remove1 a xs) = multiset_of xs - {#a#}"
+lemma mset_remove1[simp]:
+ "mset (remove1 a xs) = mset xs - {#a#}"
by (induct xs) (auto simp add: multiset_eq_iff)
-lemma multiset_of_eq_length:
- assumes "multiset_of xs = multiset_of ys"
+lemma mset_eq_length:
+ assumes "mset xs = mset ys"
shows "length xs = length ys"
- using assms by (metis size_multiset_of)
-
-lemma multiset_of_eq_length_filter:
- assumes "multiset_of xs = multiset_of ys"
+ using assms by (metis size_mset)
+
+lemma mset_eq_length_filter:
+ assumes "mset xs = mset ys"
shows "length (filter (\<lambda>x. z = x) xs) = length (filter (\<lambda>y. z = y) ys)"
- using assms by (metis count_multiset_of)
+ using assms by (metis count_mset)
lemma fold_multiset_equiv:
assumes f: "\<And>x y. x \<in> set xs \<Longrightarrow> y \<in> set xs \<Longrightarrow> f x \<circ> f y = f y \<circ> f x"
- and equiv: "multiset_of xs = multiset_of ys"
+ and equiv: "mset xs = mset ys"
shows "List.fold f xs = List.fold f ys"
using f equiv [symmetric]
proof (induct xs arbitrary: ys)
case Nil then show ?case by simp
next
case (Cons x xs)
- then have *: "set ys = set (x # xs)" by (blast dest: multiset_of_eq_setD)
+ then have *: "set ys = set (x # xs)" by (blast dest: mset_eq_setD)
have "\<And>x y. x \<in> set ys \<Longrightarrow> y \<in> set ys \<Longrightarrow> f x \<circ> f y = f y \<circ> f x"
by (rule Cons.prems(1)) (simp_all add: *)
moreover from * have "x \<in> set ys" by simp
@@ -1085,12 +1085,12 @@
ultimately show ?case by simp
qed
-lemma multiset_of_insort [simp]:
- "multiset_of (insort x xs) = multiset_of xs + {#x#}"
+lemma mset_insort [simp]:
+ "mset (insort x xs) = mset xs + {#x#}"
by (induct xs) (simp_all add: ac_simps)
-lemma multiset_of_map:
- "multiset_of (map f xs) = image_mset f (multiset_of xs)"
+lemma mset_map:
+ "mset (map f xs) = image_mset f (mset xs)"
by (induct xs) simp_all
definition mset_set :: "'a set \<Rightarrow> 'a multiset"
@@ -1154,12 +1154,12 @@
end
-lemma multiset_of_sorted_list_of_multiset [simp]:
- "multiset_of (sorted_list_of_multiset M) = M"
+lemma mset_sorted_list_of_multiset [simp]:
+ "mset (sorted_list_of_multiset M) = M"
by (induct M) simp_all
-lemma sorted_list_of_multiset_multiset_of [simp]:
- "sorted_list_of_multiset (multiset_of xs) = sort xs"
+lemma sorted_list_of_multiset_mset [simp]:
+ "sorted_list_of_multiset (mset xs) = sort xs"
by (induct xs) simp_all
lemma finite_set_mset_mset_set[simp]:
@@ -1386,12 +1386,12 @@
context linorder
begin
-lemma multiset_of_insort [simp]:
- "multiset_of (insort_key k x xs) = {#x#} + multiset_of xs"
+lemma mset_insort [simp]:
+ "mset (insort_key k x xs) = {#x#} + mset xs"
by (induct xs) (simp_all add: ac_simps)
-lemma multiset_of_sort [simp]:
- "multiset_of (sort_key k xs) = multiset_of xs"
+lemma mset_sort [simp]:
+ "mset (sort_key k xs) = mset xs"
by (induct xs) (simp_all add: ac_simps)
text \<open>
@@ -1400,7 +1400,7 @@
\<close>
lemma properties_for_sort_key:
- assumes "multiset_of ys = multiset_of xs"
+ assumes "mset ys = mset xs"
and "\<And>k. k \<in> set ys \<Longrightarrow> filter (\<lambda>x. f k = f x) ys = filter (\<lambda>x. f k = f x) xs"
and "sorted (map f ys)"
shows "sort_key f xs = ys"
@@ -1420,14 +1420,14 @@
qed
lemma properties_for_sort:
- assumes multiset: "multiset_of ys = multiset_of xs"
+ assumes multiset: "mset ys = mset xs"
and "sorted ys"
shows "sort xs = ys"
proof (rule properties_for_sort_key)
- from multiset show "multiset_of ys = multiset_of xs" .
+ from multiset show "mset ys = mset xs" .
from \<open>sorted ys\<close> show "sorted (map (\<lambda>x. x) ys)" by simp
from multiset have "\<And>k. length (filter (\<lambda>y. k = y) ys) = length (filter (\<lambda>x. k = x) xs)"
- by (rule multiset_of_eq_length_filter)
+ by (rule mset_eq_length_filter)
then have "\<And>k. replicate (length (filter (\<lambda>y. k = y) ys)) k = replicate (length (filter (\<lambda>x. k = x) xs)) k"
by simp
then show "\<And>k. k \<in> set ys \<Longrightarrow> filter (\<lambda>y. k = y) ys = filter (\<lambda>x. k = x) xs"
@@ -1439,8 +1439,8 @@
@ [x\<leftarrow>xs. f x = f (xs ! (length xs div 2))]
@ sort_key f [x\<leftarrow>xs. f x > f (xs ! (length xs div 2))]" (is "sort_key f ?lhs = ?rhs")
proof (rule properties_for_sort_key)
- show "multiset_of ?rhs = multiset_of ?lhs"
- by (rule multiset_eqI) (auto simp add: multiset_of_filter)
+ show "mset ?rhs = mset ?lhs"
+ by (rule multiset_eqI) (auto simp add: mset_filter)
next
show "sorted (map f ?rhs)"
by (auto simp add: sorted_append intro: sorted_map_same)
@@ -1523,11 +1523,11 @@
hide_const (open) part
-lemma multiset_of_remdups_le: "multiset_of (remdups xs) \<le># multiset_of xs"
+lemma mset_remdups_le: "mset (remdups xs) \<le># mset xs"
by (induct xs) (auto intro: subset_mset.order_trans)
-lemma multiset_of_update:
- "i < length ls \<Longrightarrow> multiset_of (ls[i := v]) = multiset_of ls - {#ls ! i#} + {#v#}"
+lemma mset_update:
+ "i < length ls \<Longrightarrow> mset (ls[i := v]) = mset ls - {#ls ! i#} + {#v#}"
proof (induct ls arbitrary: i)
case Nil then show ?case by simp
next
@@ -1544,15 +1544,15 @@
apply (subst add.assoc [symmetric])
apply simp
apply (rule mset_le_multiset_union_diff_commute)
- apply (simp add: mset_le_single nth_mem_multiset_of)
+ apply (simp add: mset_le_single nth_mem_mset)
done
qed
qed
-lemma multiset_of_swap:
+lemma mset_swap:
"i < length ls \<Longrightarrow> j < length ls \<Longrightarrow>
- multiset_of (ls[j := ls ! i, i := ls ! j]) = multiset_of ls"
- by (cases "i = j") (simp_all add: multiset_of_update nth_mem_multiset_of)
+ mset (ls[j := ls ! i, i := ls ! j]) = mset ls"
+ by (cases "i = j") (simp_all add: mset_update nth_mem_mset)
subsection \<open>The multiset order\<close>
@@ -2071,51 +2071,51 @@
subsection \<open>Naive implementation using lists\<close>
-code_datatype multiset_of
+code_datatype mset
lemma [code]:
- "{#} = multiset_of []"
+ "{#} = mset []"
by simp
lemma [code]:
- "{#x#} = multiset_of [x]"
+ "{#x#} = mset [x]"
by simp
lemma union_code [code]:
- "multiset_of xs + multiset_of ys = multiset_of (xs @ ys)"
+ "mset xs + mset ys = mset (xs @ ys)"
by simp
lemma [code]:
- "image_mset f (multiset_of xs) = multiset_of (map f xs)"
- by (simp add: multiset_of_map)
+ "image_mset f (mset xs) = mset (map f xs)"
+ by (simp add: mset_map)
lemma [code]:
- "filter_mset f (multiset_of xs) = multiset_of (filter f xs)"
- by (simp add: multiset_of_filter)
+ "filter_mset f (mset xs) = mset (filter f xs)"
+ by (simp add: mset_filter)
lemma [code]:
- "multiset_of xs - multiset_of ys = multiset_of (fold remove1 ys xs)"
+ "mset xs - mset ys = mset (fold remove1 ys xs)"
by (rule sym, induct ys arbitrary: xs) (simp_all add: diff_add diff_right_commute)
lemma [code]:
- "multiset_of xs #\<inter> multiset_of ys =
- multiset_of (snd (fold (\<lambda>x (ys, zs).
+ "mset xs #\<inter> mset ys =
+ mset (snd (fold (\<lambda>x (ys, zs).
if x \<in> set ys then (remove1 x ys, x # zs) else (ys, zs)) xs (ys, [])))"
proof -
- have "\<And>zs. multiset_of (snd (fold (\<lambda>x (ys, zs).
+ have "\<And>zs. mset (snd (fold (\<lambda>x (ys, zs).
if x \<in> set ys then (remove1 x ys, x # zs) else (ys, zs)) xs (ys, zs))) =
- (multiset_of xs #\<inter> multiset_of ys) + multiset_of zs"
+ (mset xs #\<inter> mset ys) + mset zs"
by (induct xs arbitrary: ys)
(auto simp add: mem_set_multiset_eq inter_add_right1 inter_add_right2 ac_simps)
then show ?thesis by simp
qed
lemma [code]:
- "multiset_of xs #\<union> multiset_of ys =
- multiset_of (split append (fold (\<lambda>x (ys, zs). (remove1 x ys, x # zs)) xs (ys, [])))"
+ "mset xs #\<union> mset ys =
+ mset (split append (fold (\<lambda>x (ys, zs). (remove1 x ys, x # zs)) xs (ys, [])))"
proof -
- have "\<And>zs. multiset_of (split append (fold (\<lambda>x (ys, zs). (remove1 x ys, x # zs)) xs (ys, zs))) =
- (multiset_of xs #\<union> multiset_of ys) + multiset_of zs"
+ have "\<And>zs. mset (split append (fold (\<lambda>x (ys, zs). (remove1 x ys, x # zs)) xs (ys, zs))) =
+ (mset xs #\<union> mset ys) + mset zs"
by (induct xs arbitrary: ys) (simp_all add: multiset_eq_iff)
then show ?thesis by simp
qed
@@ -2123,26 +2123,26 @@
declare in_multiset_in_set [code_unfold]
lemma [code]:
- "count (multiset_of xs) x = fold (\<lambda>y. if x = y then Suc else id) xs 0"
+ "count (mset xs) x = fold (\<lambda>y. if x = y then Suc else id) xs 0"
proof -
- have "\<And>n. fold (\<lambda>y. if x = y then Suc else id) xs n = count (multiset_of xs) x + n"
+ have "\<And>n. fold (\<lambda>y. if x = y then Suc else id) xs n = count (mset xs) x + n"
by (induct xs) simp_all
then show ?thesis by simp
qed
-declare set_mset_multiset_of [code]
-
-declare sorted_list_of_multiset_multiset_of [code]
+declare set_mset_mset [code]
+
+declare sorted_list_of_multiset_mset [code]
lemma [code]: -- \<open>not very efficient, but representation-ignorant!\<close>
- "mset_set A = multiset_of (sorted_list_of_set A)"
+ "mset_set A = mset (sorted_list_of_set A)"
apply (cases "finite A")
apply simp_all
apply (induct A rule: finite_induct)
apply (simp_all add: add.commute)
done
-declare size_multiset_of [code]
+declare size_mset [code]
fun ms_lesseq_impl :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool option" where
"ms_lesseq_impl [] ys = Some (ys \<noteq> [])"
@@ -2150,9 +2150,9 @@
None \<Rightarrow> None
| Some (ys1,_,ys2) \<Rightarrow> ms_lesseq_impl xs (ys1 @ ys2))"
-lemma ms_lesseq_impl: "(ms_lesseq_impl xs ys = None \<longleftrightarrow> \<not> multiset_of xs \<le># multiset_of ys) \<and>
- (ms_lesseq_impl xs ys = Some True \<longleftrightarrow> multiset_of xs <# multiset_of ys) \<and>
- (ms_lesseq_impl xs ys = Some False \<longrightarrow> multiset_of xs = multiset_of ys)"
+lemma ms_lesseq_impl: "(ms_lesseq_impl xs ys = None \<longleftrightarrow> \<not> mset xs \<le># mset ys) \<and>
+ (ms_lesseq_impl xs ys = Some True \<longleftrightarrow> mset xs <# mset ys) \<and>
+ (ms_lesseq_impl xs ys = Some False \<longrightarrow> mset xs = mset ys)"
proof (induct xs arbitrary: ys)
case (Nil ys)
show ?case by (auto simp: mset_less_empty_nonempty)
@@ -2163,13 +2163,13 @@
case None
hence x: "x \<notin> set ys" by (simp add: extract_None_iff)
{
- assume "multiset_of (x # xs) \<le># multiset_of ys"
+ assume "mset (x # xs) \<le># mset ys"
from set_mset_mono[OF this] x have False by simp
} note nle = this
moreover
{
- assume "multiset_of (x # xs) <# multiset_of ys"
- hence "multiset_of (x # xs) \<le># multiset_of ys" by auto
+ assume "mset (x # xs) <# mset ys"
+ hence "mset (x # xs) \<le># mset ys" by auto
from nle[OF this] have False .
}
ultimately show ?thesis using None by auto
@@ -2178,7 +2178,7 @@
obtain ys1 y ys2 where res: "res = (ys1,y,ys2)" by (cases res, auto)
note Some = Some[unfolded res]
from extract_SomeE[OF Some] have "ys = ys1 @ x # ys2" by simp
- hence id: "multiset_of ys = multiset_of (ys1 @ ys2) + {#x#}"
+ hence id: "mset ys = mset (ys1 @ ys2) + {#x#}"
by (auto simp: ac_simps)
show ?thesis unfolding ms_lesseq_impl.simps
unfolding Some option.simps split
@@ -2188,10 +2188,10 @@
qed
qed
-lemma [code]: "multiset_of xs \<le># multiset_of ys \<longleftrightarrow> ms_lesseq_impl xs ys \<noteq> None"
+lemma [code]: "mset xs \<le># mset ys \<longleftrightarrow> ms_lesseq_impl xs ys \<noteq> None"
using ms_lesseq_impl[of xs ys] by (cases "ms_lesseq_impl xs ys", auto)
-lemma [code]: "multiset_of xs <# multiset_of ys \<longleftrightarrow> ms_lesseq_impl xs ys = Some True"
+lemma [code]: "mset xs <# mset ys \<longleftrightarrow> ms_lesseq_impl xs ys = Some True"
using ms_lesseq_impl[of xs ys] by (cases "ms_lesseq_impl xs ys", auto)
instantiation multiset :: (equal) equal
@@ -2199,7 +2199,7 @@
definition
[code del]: "HOL.equal A (B :: 'a multiset) \<longleftrightarrow> A = B"
-lemma [code]: "HOL.equal (multiset_of xs) (multiset_of ys) \<longleftrightarrow> ms_lesseq_impl xs ys = Some False"
+lemma [code]: "HOL.equal (mset xs) (mset ys) \<longleftrightarrow> ms_lesseq_impl xs ys = Some False"
unfolding equal_multiset_def
using ms_lesseq_impl[of xs ys] by (cases "ms_lesseq_impl xs ys", auto)
@@ -2208,13 +2208,13 @@
end
lemma [code]:
- "msetsum (multiset_of xs) = listsum xs"
+ "msetsum (mset xs) = listsum xs"
by (induct xs) (simp_all add: add.commute)
lemma [code]:
- "msetprod (multiset_of xs) = fold times xs 1"
+ "msetprod (mset xs) = fold times xs 1"
proof -
- have "\<And>x. fold times xs x = msetprod (multiset_of xs) * x"
+ have "\<And>x. fold times xs x = msetprod (mset xs) * x"
by (induct xs) (simp_all add: mult.assoc)
then show ?thesis by simp
qed
@@ -2229,7 +2229,7 @@
definition (in term_syntax)
msetify :: "'a\<Colon>typerep list \<times> (unit \<Rightarrow> Code_Evaluation.term)
\<Rightarrow> 'a multiset \<times> (unit \<Rightarrow> Code_Evaluation.term)" where
- [code_unfold]: "msetify xs = Code_Evaluation.valtermify multiset_of {\<cdot>} xs"
+ [code_unfold]: "msetify xs = Code_Evaluation.valtermify mset {\<cdot>} xs"
notation fcomp (infixl "\<circ>>" 60)
notation scomp (infixl "\<circ>\<rightarrow>" 60)
@@ -2264,12 +2264,12 @@
subsection \<open>BNF setup\<close>
definition rel_mset where
- "rel_mset R X Y \<longleftrightarrow> (\<exists>xs ys. multiset_of xs = X \<and> multiset_of ys = Y \<and> list_all2 R xs ys)"
-
-lemma multiset_of_zip_take_Cons_drop_twice:
+ "rel_mset R X Y \<longleftrightarrow> (\<exists>xs ys. mset xs = X \<and> mset ys = Y \<and> list_all2 R xs ys)"
+
+lemma mset_zip_take_Cons_drop_twice:
assumes "length xs = length ys" "j \<le> length xs"
- shows "multiset_of (zip (take j xs @ x # drop j xs) (take j ys @ y # drop j ys)) =
- multiset_of (zip xs ys) + {#(x, y)#}"
+ shows "mset (zip (take j xs @ x # drop j xs) (take j ys @ y # drop j ys)) =
+ mset (zip xs ys) + {#(x, y)#}"
using assms
proof (induct xs ys arbitrary: x y j rule: list_induct2)
case Nil
@@ -2288,17 +2288,17 @@
by (case_tac j) simp
hence "k \<le> length xs"
using Cons.prems by auto
- hence "multiset_of (zip (take k xs @ x # drop k xs) (take k ys @ y # drop k ys)) =
- multiset_of (zip xs ys) + {#(x, y)#}"
+ hence "mset (zip (take k xs @ x # drop k xs) (take k ys @ y # drop k ys)) =
+ mset (zip xs ys) + {#(x, y)#}"
by (rule Cons.hyps(2))
thus ?thesis
unfolding k by (auto simp: add.commute union_lcomm)
qed
qed
-lemma ex_multiset_of_zip_left:
- assumes "length xs = length ys" "multiset_of xs' = multiset_of xs"
- shows "\<exists>ys'. length ys' = length xs' \<and> multiset_of (zip xs' ys') = multiset_of (zip xs ys)"
+lemma ex_mset_zip_left:
+ assumes "length xs = length ys" "mset xs' = mset xs"
+ shows "\<exists>ys'. length ys' = length xs' \<and> mset (zip xs' ys') = mset (zip xs ys)"
using assms
proof (induct xs ys arbitrary: xs' rule: list_induct2)
case Nil
@@ -2307,57 +2307,57 @@
next
case (Cons x xs y ys xs')
obtain j where j_len: "j < length xs'" and nth_j: "xs' ! j = x"
- by (metis Cons.prems in_set_conv_nth list.set_intros(1) multiset_of_eq_setD)
+ by (metis Cons.prems in_set_conv_nth list.set_intros(1) mset_eq_setD)
def xsa \<equiv> "take j xs' @ drop (Suc j) xs'"
- have "multiset_of xs' = {#x#} + multiset_of xsa"
+ have "mset xs' = {#x#} + mset xsa"
unfolding xsa_def using j_len nth_j
by (metis (no_types) ab_semigroup_add_class.add_ac(1) append_take_drop_id Cons_nth_drop_Suc
- multiset_of.simps(2) union_code add.commute)
- hence ms_x: "multiset_of xsa = multiset_of xs"
- by (metis Cons.prems add.commute add_right_imp_eq multiset_of.simps(2))
+ mset.simps(2) union_code add.commute)
+ hence ms_x: "mset xsa = mset xs"
+ by (metis Cons.prems add.commute add_right_imp_eq mset.simps(2))
then obtain ysa where
- len_a: "length ysa = length xsa" and ms_a: "multiset_of (zip xsa ysa) = multiset_of (zip xs ys)"
+ len_a: "length ysa = length xsa" and ms_a: "mset (zip xsa ysa) = mset (zip xs ys)"
using Cons.hyps(2) by blast
def ys' \<equiv> "take j ysa @ y # drop j ysa"
have xs': "xs' = take j xsa @ x # drop j xsa"
using ms_x j_len nth_j Cons.prems xsa_def
by (metis append_eq_append_conv append_take_drop_id diff_Suc_Suc Cons_nth_drop_Suc length_Cons
- length_drop size_multiset_of)
+ length_drop size_mset)
have j_len': "j \<le> length xsa"
using j_len xs' xsa_def
by (metis add_Suc_right append_take_drop_id length_Cons length_append less_eq_Suc_le not_less)
have "length ys' = length xs'"
unfolding ys'_def using Cons.prems len_a ms_x
- by (metis add_Suc_right append_take_drop_id length_Cons length_append multiset_of_eq_length)
- moreover have "multiset_of (zip xs' ys') = multiset_of (zip (x # xs) (y # ys))"
+ by (metis add_Suc_right append_take_drop_id length_Cons length_append mset_eq_length)
+ moreover have "mset (zip xs' ys') = mset (zip (x # xs) (y # ys))"
unfolding xs' ys'_def
- by (rule trans[OF multiset_of_zip_take_Cons_drop_twice])
+ by (rule trans[OF mset_zip_take_Cons_drop_twice])
(auto simp: len_a ms_a j_len' add.commute)
ultimately show ?case
by blast
qed
lemma list_all2_reorder_left_invariance:
- assumes rel: "list_all2 R xs ys" and ms_x: "multiset_of xs' = multiset_of xs"
- shows "\<exists>ys'. list_all2 R xs' ys' \<and> multiset_of ys' = multiset_of ys"
+ assumes rel: "list_all2 R xs ys" and ms_x: "mset xs' = mset xs"
+ shows "\<exists>ys'. list_all2 R xs' ys' \<and> mset ys' = mset ys"
proof -
have len: "length xs = length ys"
using rel list_all2_conv_all_nth by auto
obtain ys' where
- len': "length xs' = length ys'" and ms_xy: "multiset_of (zip xs' ys') = multiset_of (zip xs ys)"
- using len ms_x by (metis ex_multiset_of_zip_left)
+ len': "length xs' = length ys'" and ms_xy: "mset (zip xs' ys') = mset (zip xs ys)"
+ using len ms_x by (metis ex_mset_zip_left)
have "list_all2 R xs' ys'"
- using assms(1) len' ms_xy unfolding list_all2_iff by (blast dest: multiset_of_eq_setD)
- moreover have "multiset_of ys' = multiset_of ys"
- using len len' ms_xy map_snd_zip multiset_of_map by metis
+ using assms(1) len' ms_xy unfolding list_all2_iff by (blast dest: mset_eq_setD)
+ moreover have "mset ys' = mset ys"
+ using len len' ms_xy map_snd_zip mset_map by metis
ultimately show ?thesis
by blast
qed
-lemma ex_multiset_of: "\<exists>xs. multiset_of xs = X"
- by (induct X) (simp, metis multiset_of.simps(2))
+lemma ex_mset: "\<exists>xs. mset xs = X"
+ by (induct X) (simp, metis mset.simps(2))
bnf "'a multiset"
map: image_mset
@@ -2403,19 +2403,19 @@
unfolding rel_mset_def[abs_def] BNF_Def.Grp_def OO_def
apply (rule ext)+
apply auto
- apply (rule_tac x = "multiset_of (zip xs ys)" in exI; auto)
- apply (metis list_all2_lengthD map_fst_zip multiset_of_map)
+ apply (rule_tac x = "mset (zip xs ys)" in exI; auto)
+ apply (metis list_all2_lengthD map_fst_zip mset_map)
apply (auto simp: list_all2_iff)[1]
- apply (metis list_all2_lengthD map_snd_zip multiset_of_map)
+ apply (metis list_all2_lengthD map_snd_zip mset_map)
apply (auto simp: list_all2_iff)[1]
apply (rename_tac XY)
- apply (cut_tac X = XY in ex_multiset_of)
+ apply (cut_tac X = XY in ex_mset)
apply (erule exE)
apply (rename_tac xys)
apply (rule_tac x = "map fst xys" in exI)
- apply (auto simp: multiset_of_map)
+ apply (auto simp: mset_map)
apply (rule_tac x = "map snd xys" in exI)
- apply (auto simp: multiset_of_map list_all2I subset_eq zip_map_fst_snd)
+ apply (auto simp: mset_map list_all2I subset_eq zip_map_fst_snd)
done
next
show "\<And>z. z \<in> set_mset {#} \<Longrightarrow> False"
--- a/src/HOL/Library/Permutation.thy Thu Jun 18 16:17:51 2015 +0200
+++ b/src/HOL/Library/Permutation.thy Fri Jun 19 15:55:22 2015 +0200
@@ -120,7 +120,7 @@
apply (blast intro: perm_append_swap)
done
-lemma multiset_of_eq_perm: "multiset_of xs = multiset_of ys \<longleftrightarrow> xs <~~> ys"
+lemma mset_eq_perm: "mset xs = mset ys \<longleftrightarrow> xs <~~> ys"
apply (rule iffI)
apply (erule_tac [2] perm.induct)
apply (simp_all add: union_ac)
@@ -140,15 +140,15 @@
apply simp
done
-lemma multiset_of_le_perm_append: "multiset_of xs \<le># multiset_of ys \<longleftrightarrow> (\<exists>zs. xs @ zs <~~> ys)"
- apply (auto simp: multiset_of_eq_perm[THEN sym] mset_le_exists_conv)
- apply (insert surj_multiset_of)
+lemma mset_le_perm_append: "mset xs \<le># mset ys \<longleftrightarrow> (\<exists>zs. xs @ zs <~~> ys)"
+ apply (auto simp: mset_eq_perm[THEN sym] mset_le_exists_conv)
+ apply (insert surj_mset)
apply (drule surjD)
apply (blast intro: sym)+
done
lemma perm_set_eq: "xs <~~> ys \<Longrightarrow> set xs = set ys"
- by (metis multiset_of_eq_perm multiset_of_eq_setD)
+ by (metis mset_eq_perm mset_eq_setD)
lemma perm_distinct_iff: "xs <~~> ys \<Longrightarrow> distinct xs = distinct ys"
apply (induct pred: perm)
--- a/src/HOL/Library/Tree_Multiset.thy Thu Jun 18 16:17:51 2015 +0200
+++ b/src/HOL/Library/Tree_Multiset.thy Fri Jun 19 15:55:22 2015 +0200
@@ -26,10 +26,10 @@
lemma mset_iff_set_tree: "x \<in># mset_tree t \<longleftrightarrow> x \<in> set_tree t"
by(induction t arbitrary: x) auto
-lemma multiset_of_preorder[simp]: "multiset_of (preorder t) = mset_tree t"
+lemma mset_preorder[simp]: "mset (preorder t) = mset_tree t"
by (induction t) (auto simp: ac_simps)
-lemma multiset_of_inorder[simp]: "multiset_of (inorder t) = mset_tree t"
+lemma mset_inorder[simp]: "mset (inorder t) = mset_tree t"
by (induction t) (auto simp: ac_simps)
lemma map_mirror: "mset_tree (mirror t) = mset_tree t"
--- a/src/HOL/Probability/ex/Koepf_Duermuth_Countermeasure.thy Thu Jun 18 16:17:51 2015 +0200
+++ b/src/HOL/Probability/ex/Koepf_Duermuth_Countermeasure.thy Fri Jun 19 15:55:22 2015 +0200
@@ -239,9 +239,9 @@
assumes "t xs = t ys"
shows "\<exists>f. bij_betw f {..<length xs} {..<length ys} \<and> (\<forall>i<length xs. xs ! i = ys ! (f i))"
proof -
- have "count (multiset_of xs) = count (multiset_of ys)"
- using assms by (simp add: fun_eq_iff count_multiset_of t_def)
- then have "xs <~~> ys" unfolding multiset_of_eq_perm count_inject .
+ have "count (mset xs) = count (mset ys)"
+ using assms by (simp add: fun_eq_iff count_mset t_def)
+ then have "xs <~~> ys" unfolding mset_eq_perm count_inject .
then show ?thesis by (rule permutation_Ex_bij)
qed
--- a/src/HOL/Proofs/Extraction/Euclid.thy Thu Jun 18 16:17:51 2015 +0200
+++ b/src/HOL/Proofs/Extraction/Euclid.thy Fri Jun 19 15:55:22 2015 +0200
@@ -123,7 +123,7 @@
qed
qed
-lemma dvd_prod [iff]: "n dvd (PROD m\<Colon>nat:#multiset_of (n # ns). m)"
+lemma dvd_prod [iff]: "n dvd (PROD m\<Colon>nat:#mset (n # ns). m)"
by (simp add: msetprod_Un msetprod_singleton)
definition all_prime :: "nat list \<Rightarrow> bool" where
@@ -140,13 +140,13 @@
lemma split_all_prime:
assumes "all_prime ms" and "all_prime ns"
- shows "\<exists>qs. all_prime qs \<and> (PROD m\<Colon>nat:#multiset_of qs. m) =
- (PROD m\<Colon>nat:#multiset_of ms. m) * (PROD m\<Colon>nat:#multiset_of ns. m)" (is "\<exists>qs. ?P qs \<and> ?Q qs")
+ shows "\<exists>qs. all_prime qs \<and> (PROD m\<Colon>nat:#mset qs. m) =
+ (PROD m\<Colon>nat:#mset ms. m) * (PROD m\<Colon>nat:#mset ns. m)" (is "\<exists>qs. ?P qs \<and> ?Q qs")
proof -
from assms have "all_prime (ms @ ns)"
by (simp add: all_prime_append)
- moreover from assms have "(PROD m\<Colon>nat:#multiset_of (ms @ ns). m) =
- (PROD m\<Colon>nat:#multiset_of ms. m) * (PROD m\<Colon>nat:#multiset_of ns. m)"
+ moreover from assms have "(PROD m\<Colon>nat:#mset (ms @ ns). m) =
+ (PROD m\<Colon>nat:#mset ms. m) * (PROD m\<Colon>nat:#mset ns. m)"
by (simp add: msetprod_Un)
ultimately have "?P (ms @ ns) \<and> ?Q (ms @ ns)" ..
then show ?thesis ..
@@ -154,11 +154,11 @@
lemma all_prime_nempty_g_one:
assumes "all_prime ps" and "ps \<noteq> []"
- shows "Suc 0 < (PROD m\<Colon>nat:#multiset_of ps. m)"
+ shows "Suc 0 < (PROD m\<Colon>nat:#mset ps. m)"
using `ps \<noteq> []` `all_prime ps` unfolding One_nat_def [symmetric] by (induct ps rule: list_nonempty_induct)
(simp_all add: all_prime_simps msetprod_singleton msetprod_Un prime_gt_1_nat less_1_mult del: One_nat_def)
-lemma factor_exists: "Suc 0 < n \<Longrightarrow> (\<exists>ps. all_prime ps \<and> (PROD m\<Colon>nat:#multiset_of ps. m) = n)"
+lemma factor_exists: "Suc 0 < n \<Longrightarrow> (\<exists>ps. all_prime ps \<and> (PROD m\<Colon>nat:#mset ps. m) = n)"
proof (induct n rule: nat_wf_ind)
case (1 n)
from `Suc 0 < n`
@@ -169,21 +169,21 @@
assume "\<exists>m k. Suc 0 < m \<and> Suc 0 < k \<and> m < n \<and> k < n \<and> n = m * k"
then obtain m k where m: "Suc 0 < m" and k: "Suc 0 < k" and mn: "m < n"
and kn: "k < n" and nmk: "n = m * k" by iprover
- from mn and m have "\<exists>ps. all_prime ps \<and> (PROD m\<Colon>nat:#multiset_of ps. m) = m" by (rule 1)
- then obtain ps1 where "all_prime ps1" and prod_ps1_m: "(PROD m\<Colon>nat:#multiset_of ps1. m) = m"
+ from mn and m have "\<exists>ps. all_prime ps \<and> (PROD m\<Colon>nat:#mset ps. m) = m" by (rule 1)
+ then obtain ps1 where "all_prime ps1" and prod_ps1_m: "(PROD m\<Colon>nat:#mset ps1. m) = m"
by iprover
- from kn and k have "\<exists>ps. all_prime ps \<and> (PROD m\<Colon>nat:#multiset_of ps. m) = k" by (rule 1)
- then obtain ps2 where "all_prime ps2" and prod_ps2_k: "(PROD m\<Colon>nat:#multiset_of ps2. m) = k"
+ from kn and k have "\<exists>ps. all_prime ps \<and> (PROD m\<Colon>nat:#mset ps. m) = k" by (rule 1)
+ then obtain ps2 where "all_prime ps2" and prod_ps2_k: "(PROD m\<Colon>nat:#mset ps2. m) = k"
by iprover
from `all_prime ps1` `all_prime ps2`
- have "\<exists>ps. all_prime ps \<and> (PROD m\<Colon>nat:#multiset_of ps. m) =
- (PROD m\<Colon>nat:#multiset_of ps1. m) * (PROD m\<Colon>nat:#multiset_of ps2. m)"
+ have "\<exists>ps. all_prime ps \<and> (PROD m\<Colon>nat:#mset ps. m) =
+ (PROD m\<Colon>nat:#mset ps1. m) * (PROD m\<Colon>nat:#mset ps2. m)"
by (rule split_all_prime)
with prod_ps1_m prod_ps2_k nmk show ?thesis by simp
next
assume "prime n" then have "all_prime [n]" by (simp add: all_prime_simps)
- moreover have "(PROD m\<Colon>nat:#multiset_of [n]. m) = n" by (simp add: msetprod_singleton)
- ultimately have "all_prime [n] \<and> (PROD m\<Colon>nat:#multiset_of [n]. m) = n" ..
+ moreover have "(PROD m\<Colon>nat:#mset [n]. m) = n" by (simp add: msetprod_singleton)
+ ultimately have "all_prime [n] \<and> (PROD m\<Colon>nat:#mset [n]. m) = n" ..
then show ?thesis ..
qed
qed
@@ -193,7 +193,7 @@
shows "\<exists>p. prime p \<and> p dvd n"
proof -
from N obtain ps where "all_prime ps"
- and prod_ps: "n = (PROD m\<Colon>nat:#multiset_of ps. m)" using factor_exists
+ and prod_ps: "n = (PROD m\<Colon>nat:#mset ps. m)" using factor_exists
by simp iprover
with N have "ps \<noteq> []"
by (auto simp add: all_prime_nempty_g_one msetprod_empty)
--- a/src/HOL/Quotient_Examples/FSet.thy Thu Jun 18 16:17:51 2015 +0200
+++ b/src/HOL/Quotient_Examples/FSet.thy Fri Jun 19 15:55:22 2015 +0200
@@ -338,8 +338,8 @@
case True
then have "\<And>x y. x \<in> set (remdups xs) \<Longrightarrow> y \<in> set (remdups xs) \<Longrightarrow> f x \<circ> f y = f y \<circ> f x"
by (rule rsp_foldE)
- moreover from assms have "multiset_of (remdups xs) = multiset_of (remdups ys)"
- by (simp add: set_eq_iff_multiset_of_remdups_eq)
+ moreover from assms have "mset (remdups xs) = mset (remdups ys)"
+ by (simp add: set_eq_iff_mset_remdups_eq)
ultimately have "fold f (remdups xs) = fold f (remdups ys)"
by (rule fold_multiset_equiv)
with True show ?thesis by (simp add: fold_once_fold_remdups)
--- a/src/HOL/UNITY/Comp/AllocBase.thy Thu Jun 18 16:17:51 2015 +0200
+++ b/src/HOL/UNITY/Comp/AllocBase.thy Fri Jun 19 15:55:22 2015 +0200
@@ -17,7 +17,7 @@
"tokens [] = 0"
| "tokens (x#xs) = x + tokens xs"
-abbreviation (input) "bag_of \<equiv> multiset_of"
+abbreviation (input) "bag_of \<equiv> mset"
lemma setsum_fun_mono [rule_format]:
"!!f :: nat=>nat.
--- a/src/HOL/ZF/LProd.thy Thu Jun 18 16:17:51 2015 +0200
+++ b/src/HOL/ZF/LProd.thy Fri Jun 19 15:55:22 2015 +0200
@@ -34,7 +34,7 @@
lemma lprod_subset: "S \<subseteq> R \<Longrightarrow> lprod S \<subseteq> lprod R"
by (auto intro: lprod_subset_elem)
-lemma lprod_implies_mult: "(as, bs) \<in> lprod R \<Longrightarrow> trans R \<Longrightarrow> (multiset_of as, multiset_of bs) \<in> mult R"
+lemma lprod_implies_mult: "(as, bs) \<in> lprod R \<Longrightarrow> trans R \<Longrightarrow> (mset as, mset bs) \<in> mult R"
proof (induct as bs rule: lprod.induct)
case (lprod_single a b)
note step = one_step_implies_mult[
@@ -43,9 +43,9 @@
next
case (lprod_list ah at bh bt a b)
then have transR: "trans R" by auto
- have as: "multiset_of (ah @ a # at) = multiset_of (ah @ at) + {#a#}" (is "_ = ?ma + _")
+ have as: "mset (ah @ a # at) = mset (ah @ at) + {#a#}" (is "_ = ?ma + _")
by (simp add: algebra_simps)
- have bs: "multiset_of (bh @ b # bt) = multiset_of (bh @ bt) + {#b#}" (is "_ = ?mb + _")
+ have bs: "mset (bh @ b # bt) = mset (bh @ bt) + {#b#}" (is "_ = ?mb + _")
by (simp add: algebra_simps)
from lprod_list have "(?ma, ?mb) \<in> mult R"
by auto
@@ -86,9 +86,9 @@
assumes wf_R: "wf R"
shows "wf (lprod R)"
proof -
- have subset: "lprod (R^+) \<subseteq> inv_image (mult (R^+)) multiset_of"
+ have subset: "lprod (R^+) \<subseteq> inv_image (mult (R^+)) mset"
by (auto simp add: lprod_implies_mult trans_trancl)
- note lprodtrancl = wf_subset[OF wf_inv_image[where r="mult (R^+)" and f="multiset_of",
+ note lprodtrancl = wf_subset[OF wf_inv_image[where r="mult (R^+)" and f="mset",
OF wf_mult[OF wf_trancl[OF wf_R]]], OF subset]
note lprod = wf_subset[OF lprodtrancl, where p="lprod R", OF lprod_subset, simplified]
show ?thesis by (auto intro: lprod)
--- a/src/HOL/ex/Bubblesort.thy Thu Jun 18 16:17:51 2015 +0200
+++ b/src/HOL/ex/Bubblesort.thy Fri Jun 19 15:55:22 2015 +0200
@@ -41,7 +41,7 @@
by(auto simp: size_bubble_min dest!: bubble_minD_size split: list.splits if_splits)
qed
-lemma mset_bubble_min: "multiset_of (bubble_min xs) = multiset_of xs"
+lemma mset_bubble_min: "mset (bubble_min xs) = mset xs"
apply(induction xs rule: bubble_min.induct)
apply simp
apply simp
@@ -49,19 +49,19 @@
done
lemma bubble_minD_mset:
- "bubble_min (xs) = ys \<Longrightarrow> multiset_of xs = multiset_of ys"
+ "bubble_min (xs) = ys \<Longrightarrow> mset xs = mset ys"
by(auto simp: mset_bubble_min)
lemma mset_bubblesort:
- "multiset_of (bubblesort xs) = multiset_of xs"
+ "mset (bubblesort xs) = mset xs"
apply(induction xs rule: bubblesort.induct)
apply simp
apply simp
by(auto split: list.splits if_splits dest: bubble_minD_mset)
- (metis add_eq_conv_ex mset_bubble_min multiset_of.simps(2))
+ (metis add_eq_conv_ex mset_bubble_min mset.simps(2))
lemma set_bubblesort: "set (bubblesort xs) = set xs"
-by(rule mset_bubblesort[THEN multiset_of_eq_setD])
+by(rule mset_bubblesort[THEN mset_eq_setD])
lemma bubble_min_min: "bubble_min xs = y#ys \<Longrightarrow> z \<in> set ys \<Longrightarrow> y \<le> z"
apply(induction xs arbitrary: y ys z rule: bubble_min.induct)
--- a/src/HOL/ex/MergeSort.thy Thu Jun 18 16:17:51 2015 +0200
+++ b/src/HOL/ex/MergeSort.thy Fri Jun 19 15:55:22 2015 +0200
@@ -19,8 +19,8 @@
| "merge xs [] = xs"
| "merge [] ys = ys"
-lemma multiset_of_merge [simp]:
- "multiset_of (merge xs ys) = multiset_of xs + multiset_of ys"
+lemma mset_merge [simp]:
+ "mset (merge xs ys) = mset xs + mset ys"
by (induct xs ys rule: merge.induct) (simp_all add: ac_simps)
lemma set_merge [simp]:
@@ -42,14 +42,14 @@
"sorted (msort xs)"
by (induct xs rule: msort.induct) simp_all
-lemma multiset_of_msort:
- "multiset_of (msort xs) = multiset_of xs"
+lemma mset_msort:
+ "mset (msort xs) = mset xs"
by (induct xs rule: msort.induct)
- (simp_all, metis append_take_drop_id drop_Suc_Cons multiset_of.simps(2) multiset_of_append take_Suc_Cons)
+ (simp_all, metis append_take_drop_id drop_Suc_Cons mset.simps(2) mset_append take_Suc_Cons)
theorem msort_sort:
"sort = msort"
- by (rule ext, rule properties_for_sort) (fact multiset_of_msort sorted_msort)+
+ by (rule ext, rule properties_for_sort) (fact mset_msort sorted_msort)+
end
--- a/src/HOL/ex/Quicksort.thy Thu Jun 18 16:17:51 2015 +0200
+++ b/src/HOL/ex/Quicksort.thy Fri Jun 19 15:55:22 2015 +0200
@@ -21,7 +21,7 @@
by (simp_all add: not_le)
lemma quicksort_permutes [simp]:
- "multiset_of (quicksort xs) = multiset_of xs"
+ "mset (quicksort xs) = mset xs"
by (induct xs rule: quicksort.induct) (simp_all add: ac_simps)
lemma set_quicksort [simp]: "set (quicksort xs) = set xs"