--- a/src/HOL/List.thy Fri Dec 02 16:05:31 2005 +0100
+++ b/src/HOL/List.thy Fri Dec 02 16:43:42 2005 +0100
@@ -848,7 +848,7 @@
(\<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:
+lemma filter_cong[recdef_cong]:
"xs = ys \<Longrightarrow> (\<And>x. x \<in> set ys \<Longrightarrow> P x = Q x) \<Longrightarrow> filter P xs = filter Q ys"
apply simp
apply(erule thin_rl)
@@ -1322,6 +1322,16 @@
apply auto
done
+lemma takeWhile_cong [recdef_cong]:
+ "[| l = k; !!x. x : set l ==> P x = Q x |]
+ ==> takeWhile P l = takeWhile Q k"
+ by (induct k fixing: l, simp_all)
+
+lemma dropWhile_cong [recdef_cong]:
+ "[| l = k; !!x. x : set l ==> P x = Q x |]
+ ==> dropWhile P l = dropWhile Q k"
+ by (induct k fixing: l, simp_all)
+
subsubsection {* @{text zip} *}
@@ -1540,6 +1550,16 @@
lemma foldr_append[simp]: "foldr f (xs @ ys) a = foldr f xs (foldr f ys a)"
by (induct xs) auto
+lemma foldl_cong [recdef_cong]:
+ "[| a = b; l = k; !!a x. x : set l ==> f a x = g a x |]
+ ==> foldl f a l = foldl g b k"
+ by (induct k fixing: a b l, simp_all)
+
+lemma foldr_cong [recdef_cong]:
+ "[| a = b; l = k; !!a x. x : set l ==> f x a = g x a |]
+ ==> foldr f l a = foldr g k b"
+ by (induct k fixing: a b l, simp_all)
+
lemma foldr_foldl: "foldr f xs a = foldl (%x y. f y x) a (rev xs)"
by (induct xs) auto