summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

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"