author krauss Fri, 02 Dec 2005 16:43:42 +0100 changeset 18336 1a2e30b37ed3 parent 18335 99baddf6b0d0 child 18337 5d24dbd5e93d
Added recdef congruence rules for bounded quantifiers and commonly used higher order functions.
 src/HOL/List.thy file | annotate | diff | comparison | revisions src/HOL/Recdef.thy file | annotate | diff | comparison | revisions
```--- 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"```