# HG changeset patch
# User nipkow
# Date 1682822249 -36000
# Node ID d28dcd57d2f341e8e1c9f0735296f1bbc80a25f1
# Parent  5016262a2384997c30d49f5d05a7aa3e0131b2a0
added lemma

diff -r 5016262a2384 -r d28dcd57d2f3 src/HOL/Data_Structures/Sorting.thy
--- a/src/HOL/Data_Structures/Sorting.thy	Thu Apr 27 11:58:38 2023 +0200
+++ b/src/HOL/Data_Structures/Sorting.thy	Sun Apr 30 12:37:29 2023 +1000
@@ -443,4 +443,31 @@
   qed
 qed
 
+
+subsection \<open>Uniqueness of Sorting\<close>
+
+lemma sorting_unique:
+  assumes "mset ys = mset xs" "sorted xs" "sorted ys"
+  shows "xs = ys"
+  using assms
+proof (induction xs arbitrary: ys)
+  case (Cons x xs ys')
+  obtain y ys where ys': "ys' = y # ys"
+    using Cons.prems by (cases ys') auto
+  have "x = y"
+    using Cons.prems unfolding ys'
+  proof (induction x y arbitrary: xs ys rule: linorder_wlog)
+    case (le x y xs ys)
+    have "x \<in># mset (x # xs)"
+      by simp
+    also have "mset (x # xs) = mset (y # ys)"
+      using le by simp
+    finally show "x = y"
+      using le by auto
+  qed (simp_all add: eq_commute)
+  thus ?case
+    using Cons.prems Cons.IH[of ys] by (auto simp: ys')
+qed auto
+
+
 end