# HG changeset patch
# User haftmann
# Date 1264945892 -3600
# Node ID 874150ddd50a245984116a2d34db47648497bff3
# Parent  27ceb64d41ead0802363ffec05f9468b43170dc6
canonical insert operation; generalized lemma foldl_apply_inv to foldl_apply

diff -r 27ceb64d41ea -r 874150ddd50a src/HOL/List.thy
--- 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"