# HG changeset patch
# User nipkow
# Date 1606901459 -3600
# Node ID 83c6d29a241250e67807cedc733a12af51002a4c
# Parent  51683cd9d7fa7c71c88e6131afdae3034fe898f8# Parent  9bd2ed5e83f3859c3716b9e3a219c632d9db2fb8
merged

diff -r 51683cd9d7fa -r 83c6d29a2412 src/HOL/Data_Structures/Sorting.thy
--- a/src/HOL/Data_Structures/Sorting.thy	Tue Dec 01 20:47:19 2020 +0100
+++ b/src/HOL/Data_Structures/Sorting.thy	Wed Dec 02 10:30:59 2020 +0100
@@ -271,16 +271,19 @@
 
 subsubsection "Functional Correctness"
 
+abbreviation mset_mset :: "'a list list \<Rightarrow> 'a multiset" where
+"mset_mset xss \<equiv> \<Union># (image_mset mset (mset xss))"
+
 lemma mset_merge_adj:
-  "\<Union># (image_mset mset (mset (merge_adj xss))) = \<Union># (image_mset mset (mset xss))"
+  "mset_mset (merge_adj xss) = mset_mset xss"
 by(induction xss rule: merge_adj.induct) (auto simp: mset_merge)
 
 lemma mset_merge_all:
-  "mset (merge_all xss) = (\<Union># (mset (map mset xss)))"
+  "mset (merge_all xss) = mset_mset xss"
 by(induction xss rule: merge_all.induct) (auto simp: mset_merge mset_merge_adj)
 
 lemma mset_msort_bu: "mset (msort_bu xs) = mset xs"
-by(simp add: msort_bu_def mset_merge_all comp_def)
+by(simp add: msort_bu_def mset_merge_all multiset.map_comp comp_def)
 
 lemma sorted_merge_adj:
   "\<forall>xs \<in> set xss. sorted xs \<Longrightarrow> \<forall>xs \<in> set (merge_adj xss). sorted xs"