1.1 --- a/src/HOL/List.thy	Sun Jan 31 14:51:32 2010 +0100
     1.2 +++ b/src/HOL/List.thy	Sun Jan 31 14:51:32 2010 +0100
     1.3 @@ -167,6 +167,12 @@
     1.4      "remdups [] = []"
     1.5    | "remdups (x # xs) = (if x \<in> set xs then remdups xs else x # remdups xs)"
     1.6  
     1.7 +definition
     1.8 +  insert :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where
     1.9 +  "insert x xs = (if x \<in> set xs then xs else x # xs)"
    1.10 +
    1.11 +hide (open) const insert hide (open) fact insert_def
    1.12 +
    1.13  primrec
    1.14    remove1 :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where
    1.15      "remove1 x [] = []"
    1.16 @@ -242,6 +248,8 @@
    1.17  @{lemma "dropWhile (%n::nat. n<3) [1,2,3,0] = [3,0]" by simp}\\
    1.18  @{lemma "distinct [2,0,1::nat]" by simp}\\
    1.19  @{lemma "remdups [2,0,2,1::nat,2] = [0,1,2]" by simp}\\
    1.20 +@{lemma "List.insert 2 [0::nat,1,2] = [0,1,2]" by (simp add: List.insert_def)}\\
    1.21 +@{lemma "List.insert 3 [0::nat,1,2] = [3, 0,1,2]" by (simp add: List.insert_def)}\\
    1.22  @{lemma "remove1 2 [2,0,2,1::nat,2] = [0,2,1,2]" by simp}\\
    1.23  @{lemma "removeAll 2 [2,0,2,1::nat,2] = [0,1]" by simp}\\
    1.24  @{lemma "nth [a,b,c,d] 2 = c" by simp}\\
    1.25 @@ -1899,6 +1907,23 @@
    1.26  "length (zip xs ys) = min (length xs) (length ys)"
    1.27  by (induct xs ys rule:list_induct2') auto
    1.28  
    1.29 +lemma zip_obtain_same_length:
    1.30 +  assumes "\<And>zs ws n. length zs = length ws \<Longrightarrow> n = min (length xs) (length ys)
    1.31 +    \<Longrightarrow> zs = take n xs \<Longrightarrow> ws = take n ys \<Longrightarrow> P (zip zs ws)"
    1.32 +  shows "P (zip xs ys)"
    1.33 +proof -
    1.34 +  let ?n = "min (length xs) (length ys)"
    1.35 +  have "P (zip (take ?n xs) (take ?n ys))"
    1.36 +    by (rule assms) simp_all
    1.37 +  moreover have "zip xs ys = zip (take ?n xs) (take ?n ys)"
    1.38 +  proof (induct xs arbitrary: ys)
    1.39 +    case Nil then show ?case by simp
    1.40 +  next
    1.41 +    case (Cons x xs) then show ?case by (cases ys) simp_all
    1.42 +  qed
    1.43 +  ultimately show ?thesis by simp
    1.44 +qed
    1.45 +
    1.46  lemma zip_append1:
    1.47  "zip (xs @ ys) zs =
    1.48  zip xs (take (length xs) zs) @ zip ys (drop (length xs) zs)"
    1.49 @@ -2213,10 +2238,10 @@
    1.50    "foldl g a (map f xs) = foldl (%a x. g a (f x)) a xs"
    1.51  by(induct xs arbitrary:a) simp_all
    1.52  
    1.53 -lemma foldl_apply_inv:
    1.54 -  assumes "\<And>x. g (h x) = x"
    1.55 -  shows "foldl f (g s) xs = g (foldl (\<lambda>s x. h (f (g s) x)) s xs)"
    1.56 -  by (rule sym, induct xs arbitrary: s) (simp_all add: assms)
    1.57 +lemma foldl_apply:
    1.58 +  assumes "\<And>x. x \<in> set xs \<Longrightarrow> f x \<circ> h = h \<circ> g x"
    1.59 +  shows "foldl (\<lambda>s x. f x s) (h s) xs = h (foldl (\<lambda>s x. g x s) s xs)"
    1.60 +  by (rule sym, insert assms, induct xs arbitrary: s) (simp_all add: expand_fun_eq)
    1.61  
    1.62  lemma foldl_cong [fundef_cong, recdef_cong]:
    1.63    "[| a = b; l = k; !!a x. x : set l ==> f a x = g a x |] 
    1.64 @@ -2282,6 +2307,12 @@
    1.65    "\<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)"
    1.66    by (induct xs arbitrary: x, simp_all)
    1.67  
    1.68 +lemma foldl_weak_invariant:
    1.69 +  assumes "P s"
    1.70 +    and "\<And>s x. x \<in> set xs \<Longrightarrow> P s \<Longrightarrow> P (f s x)"
    1.71 +  shows "P (foldl f s xs)"
    1.72 +  using assms by (induct xs arbitrary: s) simp_all
    1.73 +
    1.74  text {* @{const foldl} and @{const concat} *}
    1.75  
    1.76  lemma foldl_conv_concat:
    1.77 @@ -2804,6 +2835,25 @@
    1.78    from length_remdups_concat[of "[xs]"] show ?thesis unfolding xs by simp
    1.79  qed
    1.80  
    1.81 +subsubsection {* @{const insert} *}
    1.82 +
    1.83 +lemma in_set_insert [simp]:
    1.84 +  "x \<in> set xs \<Longrightarrow> List.insert x xs = xs"
    1.85 +  by (simp add: List.insert_def)
    1.86 +
    1.87 +lemma not_in_set_insert [simp]:
    1.88 +  "x \<notin> set xs \<Longrightarrow> List.insert x xs = x # xs"
    1.89 +  by (simp add: List.insert_def)
    1.90 +
    1.91 +lemma insert_Nil [simp]:
    1.92 +  "List.insert x [] = [x]"
    1.93 +  by simp
    1.94 +
    1.95 +lemma set_insert:
    1.96 +  "set (List.insert x xs) = insert x (set xs)"
    1.97 +  by (auto simp add: List.insert_def)
    1.98 +
    1.99 +
   1.100  subsubsection {* @{text remove1} *}
   1.101  
   1.102  lemma remove1_append:
   1.103 @@ -2852,6 +2902,14 @@
   1.104  
   1.105  subsubsection {* @{text removeAll} *}
   1.106  
   1.107 +lemma removeAll_filter_not_eq:
   1.108 +  "removeAll x = filter (\<lambda>y. x \<noteq> y)"
   1.109 +proof
   1.110 +  fix xs
   1.111 +  show "removeAll x xs = filter (\<lambda>y. x \<noteq> y) xs"
   1.112 +    by (induct xs) auto
   1.113 +qed
   1.114 +
   1.115  lemma removeAll_append[simp]:
   1.116    "removeAll x (xs @ ys) = removeAll x xs @ removeAll x ys"
   1.117  by (induct xs) auto
   1.118 @@ -2871,6 +2929,9 @@
   1.119    "\<not> P x \<Longrightarrow> removeAll x (filter P xs) = filter P xs"
   1.120  by(induct xs) auto
   1.121  
   1.122 +lemma distinct_removeAll:
   1.123 +  "distinct xs \<Longrightarrow> distinct (removeAll x xs)"
   1.124 +  by (simp add: removeAll_filter_not_eq)
   1.125  
   1.126  lemma distinct_remove1_removeAll:
   1.127    "distinct xs ==> remove1 x xs = removeAll x xs"