240 @{lemma "drop 6 [a,b,c,d] = []" by simp}\\ 
246 @{lemma "drop 6 [a,b,c,d] = []" by simp}\\ 
241 @{lemma "takeWhile (%n::nat. n<3) [1,2,3,0] = [1,2]" by simp}\\ 
247 @{lemma "takeWhile (%n::nat. n<3) [1,2,3,0] = [1,2]" by simp}\\ 
242 @{lemma "dropWhile (%n::nat. n<3) [1,2,3,0] = [3,0]" by simp}\\ 
248 @{lemma "dropWhile (%n::nat. n<3) [1,2,3,0] = [3,0]" by simp}\\ 
243 @{lemma "distinct [2,0,1::nat]" by simp}\\ 
249 @{lemma "distinct [2,0,1::nat]" by simp}\\ 
244 @{lemma "remdups [2,0,2,1::nat,2] = [0,1,2]" by simp}\\ 
250 @{lemma "remdups [2,0,2,1::nat,2] = [0,1,2]" by simp}\\ 

251 @{lemma "List.insert 2 [0::nat,1,2] = [0,1,2]" by (simp add: List.insert_def)}\\ 

252 @{lemma "List.insert 3 [0::nat,1,2] = [3, 0,1,2]" by (simp add: List.insert_def)}\\ 
245 @{lemma "remove1 2 [2,0,2,1::nat,2] = [0,2,1,2]" by simp}\\ 
253 @{lemma "remove1 2 [2,0,2,1::nat,2] = [0,2,1,2]" by simp}\\ 
246 @{lemma "removeAll 2 [2,0,2,1::nat,2] = [0,1]" by simp}\\ 
254 @{lemma "removeAll 2 [2,0,2,1::nat,2] = [0,1]" by simp}\\ 
247 @{lemma "nth [a,b,c,d] 2 = c" by simp}\\ 
255 @{lemma "nth [a,b,c,d] 2 = c" by simp}\\ 
248 @{lemma "[a,b,c,d][2 := x] = [a,b,x,d]" by simp}\\ 
256 @{lemma "[a,b,c,d][2 := x] = [a,b,x,d]" by simp}\\ 
249 @{lemma "sublist [a,b,c,d,e] {0,2,3} = [a,c,d]" by (simp add:sublist_def)}\\ 
257 @{lemma "sublist [a,b,c,d,e] {0,2,3} = [a,c,d]" by (simp add:sublist_def)}\\ 
1897 
1905 
1898 lemma length_zip [simp]: 
1906 lemma length_zip [simp]: 
1899 "length (zip xs ys) = min (length xs) (length ys)" 
1907 "length (zip xs ys) = min (length xs) (length ys)" 
1900 by (induct xs ys rule:list_induct2') auto 
1908 by (induct xs ys rule:list_induct2') auto 
1901 
1909 

1910 lemma zip_obtain_same_length: 

1911 assumes "\<And>zs ws n. length zs = length ws \<Longrightarrow> n = min (length xs) (length ys) 

1912 \<Longrightarrow> zs = take n xs \<Longrightarrow> ws = take n ys \<Longrightarrow> P (zip zs ws)" 

1913 shows "P (zip xs ys)" 

1914 proof  

1915 let ?n = "min (length xs) (length ys)" 

1916 have "P (zip (take ?n xs) (take ?n ys))" 

1917 by (rule assms) simp_all 

1918 moreover have "zip xs ys = zip (take ?n xs) (take ?n ys)" 

1919 proof (induct xs arbitrary: ys) 

1920 case Nil then show ?case by simp 

1921 next 

1922 case (Cons x xs) then show ?case by (cases ys) simp_all 

1923 qed 

1924 ultimately show ?thesis by simp 

1925 qed 

1926 
1902 lemma zip_append1: 
1927 lemma zip_append1: 
1903 "zip (xs @ ys) zs = 
1928 "zip (xs @ ys) zs = 
1904 zip xs (take (length xs) zs) @ zip ys (drop (length xs) zs)" 
1929 zip xs (take (length xs) zs) @ zip ys (drop (length xs) zs)" 
1905 by (induct xs zs rule:list_induct2') auto 
1930 by (induct xs zs rule:list_induct2') auto 
1906 
1931 
2211 text{* For efficient code generation: avoid intermediate list. *} 
2236 text{* For efficient code generation: avoid intermediate list. *} 
2212 lemma foldl_map[code_unfold]: 
2237 lemma foldl_map[code_unfold]: 
2213 "foldl g a (map f xs) = foldl (%a x. g a (f x)) a xs" 
2238 "foldl g a (map f xs) = foldl (%a x. g a (f x)) a xs" 
2214 by(induct xs arbitrary:a) simp_all 
2239 by(induct xs arbitrary:a) simp_all 
2215 
2240 
2216 lemma foldl_apply_inv: 
2241 lemma foldl_apply: 
2217 assumes "\<And>x. g (h x) = x" 
2242 assumes "\<And>x. x \<in> set xs \<Longrightarrow> f x \<circ> h = h \<circ> g x" 
2218 shows "foldl f (g s) xs = g (foldl (\<lambda>s x. h (f (g s) x)) s xs)" 
2243 shows "foldl (\<lambda>s x. f x s) (h s) xs = h (foldl (\<lambda>s x. g x s) s xs)" 
2219 by (rule sym, induct xs arbitrary: s) (simp_all add: assms) 
2244 by (rule sym, insert assms, induct xs arbitrary: s) (simp_all add: expand_fun_eq) 
2220 
2245 
2221 lemma foldl_cong [fundef_cong, recdef_cong]: 
2246 lemma foldl_cong [fundef_cong, recdef_cong]: 
2222 "[ a = b; l = k; !!a x. x : set l ==> f a x = g a x ] 
2247 "[ a = b; l = k; !!a x. x : set l ==> f a x = g a x ] 
2223 ==> foldl f a l = foldl g b k" 
2248 ==> foldl f a l = foldl g b k" 
2224 by (induct k arbitrary: a b l) simp_all 
2249 by (induct k arbitrary: a b l) simp_all 
2279 by (induct xs, simp_all) 
2304 by (induct xs, simp_all) 
2280 
2305 
2281 lemma foldl_invariant: 
2306 lemma foldl_invariant: 
2282 "\<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)" 
2307 "\<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)" 
2283 by (induct xs arbitrary: x, simp_all) 
2308 by (induct xs arbitrary: x, simp_all) 

2309 

2310 lemma foldl_weak_invariant: 

2311 assumes "P s" 

2312 and "\<And>s x. x \<in> set xs \<Longrightarrow> P s \<Longrightarrow> P (f s x)" 

2313 shows "P (foldl f s xs)" 

2314 using assms by (induct xs arbitrary: s) simp_all 
2284 
2315 
2285 text {* @{const foldl} and @{const concat} *} 
2316 text {* @{const foldl} and @{const concat} *} 
2286 
2317 
2287 lemma foldl_conv_concat: 
2318 lemma foldl_conv_concat: 
2288 "foldl (op @) xs xss = xs @ concat xss" 
2319 "foldl (op @) xs xss = xs @ concat xss" 
2802 proof  
2833 proof  
2803 have xs: "concat[xs] = xs" by simp 
2834 have xs: "concat[xs] = xs" by simp 
2804 from length_remdups_concat[of "[xs]"] show ?thesis unfolding xs by simp 
2835 from length_remdups_concat[of "[xs]"] show ?thesis unfolding xs by simp 
2805 qed 
2836 qed 
2806 
2837 

2838 subsubsection {* @{const insert} *} 

2839 

2840 lemma in_set_insert [simp]: 

2841 "x \<in> set xs \<Longrightarrow> List.insert x xs = xs" 

2842 by (simp add: List.insert_def) 

2843 

2844 lemma not_in_set_insert [simp]: 

2845 "x \<notin> set xs \<Longrightarrow> List.insert x xs = x # xs" 

2846 by (simp add: List.insert_def) 

2847 

2848 lemma insert_Nil [simp]: 

2849 "List.insert x [] = [x]" 

2850 by simp 

2851 

2852 lemma set_insert: 

2853 "set (List.insert x xs) = insert x (set xs)" 

2854 by (auto simp add: List.insert_def) 

2855 

2856 
2807 subsubsection {* @{text remove1} *} 
2857 subsubsection {* @{text remove1} *} 
2808 
2858 
2809 lemma remove1_append: 
2859 lemma remove1_append: 
2810 "remove1 x (xs @ ys) = 
2860 "remove1 x (xs @ ys) = 
2811 (if x \<in> set xs then remove1 x xs @ ys else xs @ remove1 x ys)" 
2861 (if x \<in> set xs then remove1 x xs @ ys else xs @ remove1 x ys)" 