Added recdef congruence rules for bounded quantifiers and commonly used
higher order functions.

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

--- a/src/HOL/Recdef.thy	Fri Dec 02 16:05:31 2005 +0100
+++ b/src/HOL/Recdef.thy	Fri Dec 02 16:43:42 2005 +0100
@@ -63,7 +63,8 @@
   same_fst_def
   less_Suc_eq [THEN iffD2]
 
-lemmas [recdef_cong] = if_cong image_cong
+lemmas [recdef_cong] = 
+  if_cong image_cong INT_cong UN_cong bex_cong ball_cong imp_cong
 
 lemma let_cong [recdef_cong]:
     "M = N ==> (!!x. x = N ==> f x = g x) ==> Let M f = Let N g"