# HG changeset patch
# User nipkow
# Date 1604572578 -3600
# Node ID 74be394e2f0ab20eb8a5a80e6c729c505462af15
# Parent  58b1826354c970a9e87cae5757ef4b6fd40d0e57
eliminate add_mset

diff -r 58b1826354c9 -r 74be394e2f0a src/HOL/Data_Structures/Sorting.thy
--- a/src/HOL/Data_Structures/Sorting.thy	Wed Nov 04 07:39:17 2020 +0000
+++ b/src/HOL/Data_Structures/Sorting.thy	Thu Nov 05 11:36:18 2020 +0100
@@ -27,7 +27,7 @@
 
 subsubsection "Functional Correctness"
 
-lemma mset_insort: "mset (insort x xs) = add_mset x (mset xs)"
+lemma mset_insort: "mset (insort x xs) = {#x#} + mset xs"
 apply(induction xs)
 apply auto
 done
@@ -39,7 +39,7 @@
 done
 
 lemma set_insort: "set (insort x xs) = insert x (set xs)"
-by (metis mset_insort set_mset_add_mset_insert set_mset_mset)
+by(simp add: mset_insort flip: set_mset_mset)
 
 lemma sorted_insort: "sorted (insort a xs) = sorted xs"
 apply(induction xs)
@@ -386,7 +386,7 @@
 
 subsubsection "Standard functional correctness"
 
-lemma mset_insort_key: "mset (insort_key f x xs) = add_mset x (mset xs)"
+lemma mset_insort_key: "mset (insort_key f x xs) = {#x#} + mset xs"
 by(induction xs) simp_all
 
 lemma mset_isort_key: "mset (isort_key f xs) = mset xs"