executable sorted_list_of_multiset

--- a/src/HOL/Library/DAList.thy	Fri May 02 16:25:38 2025 +0100
+++ b/src/HOL/Library/DAList.thy	Fri May 02 17:24:43 2025 +0200
@@ -37,6 +37,10 @@
 lemma impl_of_distinct [simp, intro]: "distinct (map fst (impl_of xs))"
   using impl_of[of xs] by simp
 
+lemma impl_of_Alist:
+  \<open>impl_of (Alist xs) = xs\<close> if \<open>distinct (map fst xs)\<close>
+  using Alist_inverse [of xs] that by simp
+
 lemma Alist_impl_of [code abstype]: "Alist (impl_of xs) = xs"
   by (rule impl_of_inverse)
 

--- a/src/HOL/Library/DAList_Multiset.thy	Fri May 02 16:25:38 2025 +0100
+++ b/src/HOL/Library/DAList_Multiset.thy	Fri May 02 17:24:43 2025 +0200
@@ -157,6 +157,26 @@
 lemma count_Bag [simp, code]: "count (Bag xs) = count_of (DAList.impl_of xs)"
   by (simp add: Bag_def count_of_multiset)
 
+lemma Bag_eq:
+  \<open>Bag ms = (\<Sum>(a, n)\<leftarrow>alist.impl_of ms. replicate_mset n a)\<close>
+  for ms :: \<open>('a, nat) alist\<close>
+proof -
+  have *: \<open>count_of xs a = count (\<Sum>(a, n)\<leftarrow>xs. replicate_mset n a) a\<close>
+    if \<open>distinct (map fst xs)\<close>
+    for xs and a :: 'a
+  using that proof (induction xs)
+    case Nil
+    then show ?case
+      by simp
+  next
+    case (Cons xn xs)
+    then show ?case by (cases xn)
+      (auto simp add: count_eq_zero_iff if_split_mem2 image_iff)
+  qed
+  show ?thesis
+    by (rule multiset_eqI) (simp add: *)
+qed
+
 lemma Mempty_Bag [code]: "{#} = Bag (DAList.empty)"
   by (simp add: multiset_eq_iff alist.Alist_inverse DAList.empty_def)
 
@@ -426,6 +446,23 @@
   qed
 qed
 
+lemma sorted_list_of_multiset_Bag [code]:
+  \<open>sorted_list_of_multiset (Bag ms) = concat (map (\<lambda>(a, n). replicate n a)
+    (sort_key fst (DAList.impl_of ms)))\<close>  (is \<open>?lhs = ?rhs\<close>)
+proof -
+  have *: \<open>sorted (concat (map (\<lambda>(a, n). replicate n a) ans))\<close>
+    if \<open>sorted (map fst ans)\<close>
+    for ans :: \<open>('a \<times> nat) list\<close>
+    using that by (induction ans) (auto simp add: sorted_append)
+  have \<open>mset ?rhs = mset ?lhs\<close>
+    by (simp add: Bag_eq mset_concat comp_def split_def flip: sum_mset_sum_list)
+  moreover have \<open>sorted ?rhs\<close>
+    by (rule *) simp
+  ultimately have \<open>sort ?lhs = ?rhs\<close>
+    by (rule properties_for_sort)
+  then show ?thesis
+    by simp
+qed
 
 instantiation multiset :: (exhaustive) exhaustive
 begin

--- a/src/HOL/Library/Multiset.thy	Fri May 02 16:25:38 2025 +0100
+++ b/src/HOL/Library/Multiset.thy	Fri May 02 17:24:43 2025 +0200
@@ -2299,6 +2299,10 @@
   "set (sorted_list_of_multiset M) = set_mset M"
   by (induct M) (simp_all add: set_insort_key)
 
+lemma sorted_sorted_list_of_multiset [iff]:
+  \<open>sorted (sorted_list_of_multiset M)\<close>
+  by (induction M) (simp_all add: sorted_insort)
+
 lemma sorted_list_of_mset_set [simp]:
   "sorted_list_of_multiset (mset_set A) = sorted_list_of_set A"
   by (cases "finite A") (induct A rule: finite_induct, simp_all)
@@ -3213,6 +3217,10 @@
 
 hide_const (open) part
 
+lemma sort_sorted_list_of_multiset_eq [simp]:
+  \<open>sort (sorted_list_of_multiset M) = sorted_list_of_multiset M\<close> for M :: \<open>'a::linorder multiset\<close>
+  by (rule properties_for_sort) simp_all
+
 lemma mset_remdups_subset_eq: "mset (remdups xs) \<subseteq># mset xs"
   by (induct xs) (auto intro: subset_mset.order_trans)