# 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"