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

author | haftmann |

Sun, 31 Jan 2010 14:51:32 +0100 | |

changeset 34978 | 874150ddd50a |

parent 34977 | 27ceb64d41ea |

child 34979 | 8cb6e7a42e9c |

canonical insert operation; generalized lemma foldl_apply_inv to foldl_apply

src/HOL/List.thy | file | annotate | diff | comparison | revisions |

--- a/src/HOL/List.thy Sun Jan 31 14:51:32 2010 +0100 +++ b/src/HOL/List.thy Sun Jan 31 14:51:32 2010 +0100 @@ -167,6 +167,12 @@ "remdups [] = []" | "remdups (x # xs) = (if x \<in> set xs then remdups xs else x # remdups xs)" +definition + insert :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where + "insert x xs = (if x \<in> set xs then xs else x # xs)" + +hide (open) const insert hide (open) fact insert_def + primrec remove1 :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where "remove1 x [] = []" @@ -242,6 +248,8 @@ @{lemma "dropWhile (%n::nat. n<3) [1,2,3,0] = [3,0]" by simp}\\ @{lemma "distinct [2,0,1::nat]" by simp}\\ @{lemma "remdups [2,0,2,1::nat,2] = [0,1,2]" by simp}\\ +@{lemma "List.insert 2 [0::nat,1,2] = [0,1,2]" by (simp add: List.insert_def)}\\ +@{lemma "List.insert 3 [0::nat,1,2] = [3, 0,1,2]" by (simp add: List.insert_def)}\\ @{lemma "remove1 2 [2,0,2,1::nat,2] = [0,2,1,2]" by simp}\\ @{lemma "removeAll 2 [2,0,2,1::nat,2] = [0,1]" by simp}\\ @{lemma "nth [a,b,c,d] 2 = c" by simp}\\ @@ -1899,6 +1907,23 @@ "length (zip xs ys) = min (length xs) (length ys)" by (induct xs ys rule:list_induct2') auto +lemma zip_obtain_same_length: + assumes "\<And>zs ws n. length zs = length ws \<Longrightarrow> n = min (length xs) (length ys) + \<Longrightarrow> zs = take n xs \<Longrightarrow> ws = take n ys \<Longrightarrow> P (zip zs ws)" + shows "P (zip xs ys)" +proof - + let ?n = "min (length xs) (length ys)" + have "P (zip (take ?n xs) (take ?n ys))" + by (rule assms) simp_all + moreover have "zip xs ys = zip (take ?n xs) (take ?n ys)" + proof (induct xs arbitrary: ys) + case Nil then show ?case by simp + next + case (Cons x xs) then show ?case by (cases ys) simp_all + qed + ultimately show ?thesis by simp +qed + lemma zip_append1: "zip (xs @ ys) zs = zip xs (take (length xs) zs) @ zip ys (drop (length xs) zs)" @@ -2213,10 +2238,10 @@ "foldl g a (map f xs) = foldl (%a x. g a (f x)) a xs" by(induct xs arbitrary:a) simp_all -lemma foldl_apply_inv: - assumes "\<And>x. g (h x) = x" - shows "foldl f (g s) xs = g (foldl (\<lambda>s x. h (f (g s) x)) s xs)" - by (rule sym, induct xs arbitrary: s) (simp_all add: assms) +lemma foldl_apply: + assumes "\<And>x. x \<in> set xs \<Longrightarrow> f x \<circ> h = h \<circ> g x" + shows "foldl (\<lambda>s x. f x s) (h s) xs = h (foldl (\<lambda>s x. g x s) s xs)" + by (rule sym, insert assms, induct xs arbitrary: s) (simp_all add: expand_fun_eq) lemma foldl_cong [fundef_cong, recdef_cong]: "[| a = b; l = k; !!a x. x : set l ==> f a x = g a x |] @@ -2282,6 +2307,12 @@ "\<lbrakk>Q x ; \<forall> x\<in> set xs. P x; \<forall> x y. P x \<and> Q y \<longrightarrow> Q (f y x) \<rbrakk> \<Longrightarrow> Q (foldl f x xs)" by (induct xs arbitrary: x, simp_all) +lemma foldl_weak_invariant: + assumes "P s" + and "\<And>s x. x \<in> set xs \<Longrightarrow> P s \<Longrightarrow> P (f s x)" + shows "P (foldl f s xs)" + using assms by (induct xs arbitrary: s) simp_all + text {* @{const foldl} and @{const concat} *} lemma foldl_conv_concat: @@ -2804,6 +2835,25 @@ from length_remdups_concat[of "[xs]"] show ?thesis unfolding xs by simp qed +subsubsection {* @{const insert} *} + +lemma in_set_insert [simp]: + "x \<in> set xs \<Longrightarrow> List.insert x xs = xs" + by (simp add: List.insert_def) + +lemma not_in_set_insert [simp]: + "x \<notin> set xs \<Longrightarrow> List.insert x xs = x # xs" + by (simp add: List.insert_def) + +lemma insert_Nil [simp]: + "List.insert x [] = [x]" + by simp + +lemma set_insert: + "set (List.insert x xs) = insert x (set xs)" + by (auto simp add: List.insert_def) + + subsubsection {* @{text remove1} *} lemma remove1_append: @@ -2852,6 +2902,14 @@ subsubsection {* @{text removeAll} *} +lemma removeAll_filter_not_eq: + "removeAll x = filter (\<lambda>y. x \<noteq> y)" +proof + fix xs + show "removeAll x xs = filter (\<lambda>y. x \<noteq> y) xs" + by (induct xs) auto +qed + lemma removeAll_append[simp]: "removeAll x (xs @ ys) = removeAll x xs @ removeAll x ys" by (induct xs) auto @@ -2871,6 +2929,9 @@ "\<not> P x \<Longrightarrow> removeAll x (filter P xs) = filter P xs" by(induct xs) auto +lemma distinct_removeAll: + "distinct xs \<Longrightarrow> distinct (removeAll x xs)" + by (simp add: removeAll_filter_not_eq) lemma distinct_remove1_removeAll: "distinct xs ==> remove1 x xs = removeAll x xs"