# HG changeset patch
# User nipkow
# Date 1127589195 -7200
# Node ID f8ea8068c6d9f55c251aaddb4ac221e410288a6c
# Parent  f4e2587bc7a5a702f278dea8f4c5d69ba2843936
a few new filter lemmas

diff -r f4e2587bc7a5 -r f8ea8068c6d9 src/HOL/List.thy
--- a/src/HOL/List.thy	Sat Sep 24 16:43:41 2005 +0200
+++ b/src/HOL/List.thy	Sat Sep 24 21:13:15 2005 +0200
@@ -778,6 +778,48 @@
   qed
 qed
 
+lemma Cons_eq_filterD:
+ "x#xs = filter P ys \<Longrightarrow>
+  \<exists>us vs. ys = us @ x # vs \<and> (\<forall>u\<in>set us. \<not> P u) \<and> P x \<and> xs = filter P vs"
+  (concl is "\<exists>us vs. ?P ys us vs")
+proof(induct ys)
+  case Nil thus ?case by simp
+next
+  case (Cons y ys)
+  show ?case (is "\<exists>x. ?Q x")
+  proof cases
+    assume Py: "P y"
+    show ?thesis
+    proof cases
+      assume xy: "x = y"
+      show ?thesis
+      proof from Py xy Cons(2) show "?Q []" by simp qed
+    next
+      assume "x \<noteq> y" with Py Cons(2) show ?thesis by simp
+    qed
+  next
+    assume Py: "\<not> P y"
+    with Cons obtain us vs where 1 : "?P (y#ys) (y#us) vs" by fastsimp
+    show ?thesis (is "? us. ?Q us")
+    proof show "?Q (y#us)" using 1 by simp qed
+  qed
+qed
+
+lemma filter_eq_ConsD:
+ "filter P ys = x#xs \<Longrightarrow>
+  \<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(rule Cons_eq_filterD) simp
+
+lemma filter_eq_Cons_iff:
+ "(filter P ys = x#xs) =
+  (\<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:filter_eq_ConsD)
+
+lemma Cons_eq_filter_iff:
+ "(x#xs = filter P ys) =
+  (\<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 filter_cong:
  "xs = ys \<Longrightarrow> (\<And>x. x \<in> set ys \<Longrightarrow> P x = Q x) \<Longrightarrow> filter P xs = filter Q ys"
 apply simp