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