# HG changeset patch
# User haftmann
# Date 1440673665 -7200
# Node ID 162bd20dae23aad5479b4a83dd0764e0da48ec47
# Parent  aeb578badc1cb8dfd3bd8c71f4f27ddfd7beb727
more lemmas on sorting and multisets (due to Thomas Sewell)

diff -r aeb578badc1c -r 162bd20dae23 src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Thu Aug 27 20:16:07 2015 +0200
+++ b/src/HOL/Library/Multiset.thy	Thu Aug 27 13:07:45 2015 +0200
@@ -1169,6 +1169,10 @@
 lemma filter_eq_replicate_mset: "{#y \<in># D. y = x#} = replicate_mset (count D x) x"
   by (induct D) simp_all
 
+lemma replicate_count_mset_eq_filter_eq:
+  "replicate (count (mset xs) k) k = filter (HOL.eq k) xs"
+  by (induct xs) auto
+
 
 subsection \<open>Big operators\<close>
 
@@ -1396,6 +1400,43 @@
     by (simp add: replicate_length_filter)
 qed
 
+lemma sort_key_inj_key_eq:
+  assumes mset_equal: "mset xs = mset ys"
+    and "inj_on f (set xs)"
+    and "sorted (map f ys)"
+  shows "sort_key f xs = ys"
+proof (rule properties_for_sort_key)
+  from mset_equal
+  show "mset ys = mset xs" by simp
+  from `sorted (map f ys)`
+  show "sorted (map f ys)" .
+  show "[x\<leftarrow>ys . f k = f x] = [x\<leftarrow>xs . f k = f x]" if "k \<in> set ys" for k
+  proof -
+    from mset_equal
+    have set_equal: "set xs = set ys" by (rule mset_eq_setD)
+    with that have "insert k (set ys) = set ys" by auto
+    with `inj_on f (set xs)` have inj: "inj_on f (insert k (set ys))"
+      by (simp add: set_equal)
+    from inj have "[x\<leftarrow>ys . f k = f x] = filter (HOL.eq k) ys"
+      by (auto intro!: inj_on_filter_key_eq)
+    also have "\<dots> = replicate (count (mset ys) k) k"
+      by (simp add: replicate_count_mset_eq_filter_eq)
+    also have "\<dots> = replicate (count (mset xs) k) k"
+      using mset_equal by simp
+    also have "\<dots> = filter (HOL.eq k) xs"
+      by (simp add: replicate_count_mset_eq_filter_eq)
+    also have "\<dots> = [x\<leftarrow>xs . f k = f x]"
+      using inj by (auto intro!: inj_on_filter_key_eq [symmetric] simp add: set_equal)
+    finally show ?thesis .
+  qed
+qed
+
+lemma sort_key_eq_sort_key:
+  assumes "mset xs = mset ys"
+    and "inj_on f (set xs)"
+  shows "sort_key f xs = sort_key f ys"
+  by (rule sort_key_inj_key_eq) (simp_all add: assms)
+
 lemma sort_key_by_quicksort:
   "sort_key f xs = sort_key f [x\<leftarrow>xs. f x < f (xs ! (length xs div 2))]
     @ [x\<leftarrow>xs. f x = f (xs ! (length xs div 2))]
diff -r aeb578badc1c -r 162bd20dae23 src/HOL/List.thy
--- a/src/HOL/List.thy	Thu Aug 27 20:16:07 2015 +0200
+++ b/src/HOL/List.thy	Thu Aug 27 13:07:45 2015 +0200
@@ -1555,6 +1555,11 @@
   (\<exists>us vs. ys = us @ x # vs \<and> (\<forall>u\<in>set us. \<not> P u) \<and> P x \<and> xs = filter P vs)"
 by(auto dest:Cons_eq_filterD)
 
+lemma inj_on_filter_key_eq:
+  assumes "inj_on f (insert y (set xs))"
+  shows "[x\<leftarrow>xs . f y = f x] = filter (HOL.eq y) xs"
+  using assms by (induct xs) auto
+
 lemma filter_cong[fundef_cong]:
   "xs = ys \<Longrightarrow> (\<And>x. x \<in> set ys \<Longrightarrow> P x = Q x) \<Longrightarrow> filter P xs = filter Q ys"
 apply simp